1  /-
  2  Copyright (c) 2019 Sébastien Gouëzel. All rights reserved.
  3  Released under Apache 2.0 license as described in the file LICENSE.
  4  Author: Sébastien Gouëzel
  5  -/
  6  
  7  import topology.metric_space.closeds set_theory.cardinal topology.metric_space.gromov_hausdorff_realized
src         └───────────────────────────┘ └─────────────────┘ └─────────────────────────────────────────────┘
  8  topology.metric_space.completion
src  └──────────────────────────────┘
  9  
 10  /-!
 11  # Gromov-Hausdorff distance
 12  
 13  This file defines the Gromov-Hausdorff distance on the space of nonempty compact metric spaces
 14  up to isometry.
 15  
 16  We introduce the space of all nonempty compact metric spaces, up to isometry,
 17  called `GH_space`, and endow it with a metric space structure. The distance,
 18  known as the Gromov-Hausdorff distance, is defined as follows: given two
 19  nonempty compact spaces `X` and `Y`, their distance is the minimum Hausdorff distance
 20  between all possible isometric embeddings of `X` and `Y` in all metric spaces.
 21  To define properly the Gromov-Hausdorff space, we consider the non-empty
 22  compact subsets of `ℓ^∞(ℝ)` up to isometry, which is a well-defined type,
 23  and define the distance as the infimum of the Hausdorff distance over all
 24  embeddings in `ℓ^∞(ℝ)`. We prove that this coincides with the previous description,
 25  as all separable metric spaces embed isometrically into `ℓ^∞(ℝ)`, through an
 26  embedding called the Kuratowski embedding.
 27  To prove that we have a distance, we should show that if spaces can be coupled
 28  to be arbitrarily close, then they are isometric. More generally, the Gromov-Hausdorff
 29  distance is realized, i.e., there is a coupling for which the Hausdorff distance
 30  is exactly the Gromov-Hausdorff distance. This follows from a compactness
 31  argument, essentially following from Arzela-Ascoli.
 32  
 33  ## Main results
 34  
 35  We prove the most important properties of the Gromov-Hausdorff space: it is a polish space,
 36  i.e., it is complete and second countable. We also prove the Gromov compactness criterion.
 37  
 38  -/
 39  
 40  noncomputable theory
 41  open_locale classical topological_space
 42  universes u v w
 43  
 44  open classical lattice set function topological_space filter metric quotient
 45  open bounded_continuous_function nat Kuratowski_embedding
 46  open sum (inl inr)
 47  set_option class.instance_max_depth 50
doc             └──────────────────────┘
 48  
 49  local attribute [instance] metric_space_sum
id                              └──────────────┘
src                             └──────────────┘
typ                             └──────────────┘
doc                             └──────────────┘
 50  
 51  
 52  namespace Gromov_Hausdorff
 53  
 54  section GH_space
 55  /- In this section, we define the Gromov-Hausdorff space, denoted `GH_space` as the quotient
 56  of nonempty compact subsets of `ℓ^∞(ℝ)` by identifying isometric sets.
 57  Using the Kuratwoski embedding, we get a canonical map `to_GH_space` mapping any nonempty
 58  compact type to `GH_space`. -/
 59  
 60  /-- Equivalence relation identifying two nonempty compact sets which are isometric -/
 61  private definition isometry_rel : nonempty_compacts ℓ_infty_ℝ → nonempty_compacts ℓ_infty_ℝ → Prop :=
id                                     └───────────────┘ └───────┘   └───────────────┘ └───────┘
src                                    └───────────────┘ └───────┘   └───────────────┘ └───────┘
typ                                    └───────────────┘ └───────┘   └───────────────┘ └───────┘
doc                                    └───────────────┘ └───────┘   └───────────────┘ └───────┘
 62    λx y, nonempty (x.val ≃ᵢ y.val)
id         └──────┘  └──┘ └┘ └──┘
src          └──────┘   └──┘ └┘  └──┘
typ        └──────┘  └──┘ └┘ └──┘
doc                          └┘
 63  
 64  /-- This is indeed an equivalence relation -/
 65  private lemma is_equivalence_isometry_rel : equivalence isometry_rel :=
id                                               └─────────┘ └──────────┘
src                                              └─────────┘ └──────────┘
typ                                              └─────────┘ └──────────┘
doc                                                          └──────────┘
 66  ⟨λx, ⟨isometric.refl _⟩, λx y ⟨e⟩, ⟨e.symm⟩, λ x y z ⟨e⟩ ⟨f⟩, ⟨e.trans f⟩⟩
id        └────────────┘             └───┘               └────┘
src        └────────────┘                 └───┘                      └────┘
typ       └────────────┘             └───┘               └────┘
doc        └────────────┘                 └───┘                      └────┘
 67  
 68  /-- setoid instance identifying two isometric nonempty compact subspaces of ℓ^∞(ℝ) -/
 69  instance isometry_rel.setoid : setoid (nonempty_compacts ℓ_infty_ℝ) :=
id                                  └────┘  └───────────────┘ └───────┘
src                                 └────┘  └───────────────┘ └───────┘
typ                                 └────┘  └───────────────┘ └───────┘
doc                                         └───────────────┘ └───────┘
 70  setoid.mk isometry_rel is_equivalence_isometry_rel
id   └───────┘ └──────────┘ └─────────────────────────┘
src  └───────┘ └──────────┘ └─────────────────────────┘
typ  └───────┘ └──────────┘ └─────────────────────────┘
doc            └──────────┘ └─────────────────────────┘
 71  
 72  /-- The Gromov-Hausdorff space -/
 73  definition GH_space : Type := quotient (isometry_rel.setoid)
id                                 └──────┘  └─────────────────┘
src                                └──────┘  └─────────────────┘
typ                                └──────┘  └─────────────────┘
doc                                          └─────────────────┘
 74  
 75  /-- Map any nonempty compact type to `GH_space` -/
 76  definition to_GH_space (α : Type u) [metric_space α] [compact_space α] [nonempty α] : GH_space :=
id                                        └──────────┘    └───────────┘    └──────┘     └──────┘
src                                       └──────────┘     └───────────┘     └──────┘      └──────┘
typ                                       └──────────┘    └───────────┘    └──────┘     └──────┘
doc                                       └──────────┘     └───────────┘                   └──────┘
 77    ⟦nonempty_compacts.Kuratowski_embedding α⟧
id     └────────────────────────────────────┘ 
src    └────────────────────────────────────┘  
typ    └────────────────────────────────────┘ 
doc     └────────────────────────────────────┘
 78  
 79  instance : inhabited GH_space := ⟨quot.mk _ ⟨{0}, by simp⟩⟩
id              └───────┘ └──────┘     └─────┘    
src             └───────┘ └──────┘                       └──┘
typ             └───────┘ └──────┘     └─────┘           └──┘
doc                       └──────┘                        └──┘
txt                                                       └──┘
par                                                       └──┘
st                                                       └───┘
 80  
 81  /-- A metric space representative of any abstract point in `GH_space` -/
 82  definition GH_space.rep (p : GH_space) : Type := (quot.out p).val
id                                └──────┘             └──────┘  └─┘
src                               └──────┘             └──────┘   └─┘
typ                               └──────┘             └──────┘  └─┘
doc                               └──────┘             └──────┘
 83  
 84  lemma eq_to_GH_space_iff {α : Type u} [metric_space α] [compact_space α] [nonempty α] {p : nonempty_compacts ℓ_infty_ℝ} :
id                                          └──────────┘    └───────────┘    └──────┘        └───────────────┘ └───────┘
src                                         └──────────┘     └───────────┘     └──────┘         └───────────────┘ └───────┘
typ                                         └──────────┘    └───────────┘    └──────┘        └───────────────┘ └───────┘
doc                                         └──────────┘     └───────────┘                      └───────────────┘ └───────┘
 85    ⟦p⟧ = to_GH_space α ↔ ∃Ψ : α → ℓ_infty_ℝ, isometry Ψ ∧ range Ψ = p.val :=
id       └─────────┘         └───────┘ └──────┘   └───┘   └──┘
src       └─────────┘            └───────┘ └──────┘    └───┘     └──┘
typ      └─────────┘         └───────┘ └──────┘   └───┘   └──┘
doc          └─────────┘              └───────┘  └──────┘     └───┘
 86  begin
st   └─────
 87    simp only [to_GH_space, quotient.eq],
id                └─────────┘  └─────────┘
src    └─────────┘└─────────┘└┘└─────────┘
typ    └─────────┘└─────────┘└┘└─────────┘
doc    └─────────┘└─────────┘└┘           
txt    └─────────┘           └┘           
par    └─────────┘           └┘           
pid        └──┘└┘           └┘           
st   ─────────────────────────────────────┘└─
 88    split,
src    └───┘
typ    └───┘
doc    └───┘
txt    └───┘
par    └───┘
st   ──────┘└─
 89    { assume h,
src      └──────┘
typ      └──────┘
doc      └──────┘
txt      └──────┘
par      └──────┘
pid      └──────┘
st   ───┘└──────┘└─
 90      rcases setoid.symm h with ⟨e⟩,
id              └─────────┘ 
src      └─────┘└─────────┘ └───────┘
typ      └─────┘└─────────┘└───────┘
doc      └─────┘            └───────┘
txt      └─────┘            └───────┘
par      └─────┘            └───────┘
pid                        └───────┘
st   ────────────────────────────────┘└─
 91      have f := (Kuratowski_embedding.isometry α).isometric_on_range.trans e,
id                  └───────────────────────────┘                            
src      └────────┘ └───────────────────────────┘ └─────────────────────────┘
typ      └────────┘ └───────────────────────────┘└─────────────────────────┘
doc      └────────┘ └───────────────────────────┘ └─────────────────────────┘
txt      └────────┘                               └─────────────────────────┘
par      └────────┘                               └─────────────────────────┘
pid      └────┘└─┘                               └─────────────────────────┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
 92      use λx, f x,
id               
src      └──┘ └─┘ 
typ      └──┘ └─┘
doc      └──┘ └─┘ 
txt      └──┘ └─┘ 
par      └──┘ └─┘ 
pid          └─┘ 
st   ──────────────┘└─
 93      split,
src      └───┘
typ      └───┘
doc      └───┘
txt      └───┘
par      └───┘
st   ────────┘└─
 94      { apply isometry_subtype_val.comp f.isometry },
id               └───────────────────────┘ └────────┘
src        └────┘└───────────────────────┘└────────┘
typ        └────┘└───────────────────────┘└────────┘
doc        └────┘└───────────────────────┘          
txt        └────┘                                   
par        └────┘                                   
pid                                                
st   ─────┘└─────────────────────────────────────────┘└┘
 95      { rw [range_comp, f.range_coe, set.image_univ, set.range_coe_subtype] } },
id             └────────┘               └────────────┘  └───────────────────┘
src        └──┘└────────┘└┘           └┘└────────────┘└┘└───────────────────┘└┘
typ        └──┘└────────┘└┘└─────────┘└┘└────────────┘└┘└───────────────────┘└┘
doc        └──┘          └┘           └┘              └┘                     └┘
txt        └──┘          └┘           └┘              └┘                     └┘
par        └──┘          └┘           └┘              └┘                     └┘
pid          └┘          └┘           └┘              └┘                     
st   ───────────────────┘└───────────┘└──────────────┘└─────────────────────┘└──┘
 96    { rintros ⟨Ψ, ⟨isomΨ, rangeΨ⟩⟩,
src      └──────────────────────────┘
typ      └──────────────────────────┘
doc      └──────────────────────────┘
txt      └──────────────────────────┘
par      └──────────────────────────┘
pid             └───────────────────┘
st   ───────────────────────────────┘└─
 97      have f := ((Kuratowski_embedding.isometry α).isometric_on_range.symm.trans
id                   └───────────────────────────┘ 
src      └────────┘  └───────────────────────────┘ └───────────────────────────────
typ      └────────┘  └───────────────────────────┘└───────────────────────────────
doc      └────────┘  └───────────────────────────┘ └───────────────────────────────
txt      └────────┘                                └───────────────────────────────
par      └────────┘                                └───────────────────────────────
pid      └────┘└─┘                                └───────────────────────────────
st   ───────────────────────────────────────────────────────────────────────────────
 98                 isomΨ.isometric_on_range).symm,
id                  └──────────────────────┘
src  ──────────────┘└──────────────────────┘└────┘
typ  ──────────────┘└──────────────────────┘└────┘
doc  ──────────────┘└──────────────────────┘└────┘
txt  ──────────────┘                        └────┘
par  ──────────────┘                        └────┘
pid  ──────────────┘                        └───┘
st   ────────────────────────────────────────────┘└─
 99      have E : (range Ψ ≃ᵢ (nonempty_compacts.Kuratowski_embedding α).val) = (p.val ≃ᵢ range (Kuratowski_embedding α)),
id                        └┘  └────────────────────────────────────┘           └───┘    └───┘  └──────────────────┘ 
src      └───────┘       └┘ └────────────────────────────────────┘ └─────┘ └───┘  └───┘ └──────────────────┘ └┘
typ      └───────┘      └┘ └────────────────────────────────────┘ └─────┘ └───┘  └───┘ └──────────────────┘└┘
doc      └───────┘       └┘ └────────────────────────────────────┘ └─────┘         └───┘ └──────────────────┘ └┘
txt      └───────┘                                                 └─────┘                                    └┘
par      └───────┘                                                 └─────┘                                    └┘
pid      └────┘└─┘                                                 └─────┘                                    └┘
st   ───────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘
100        by { dunfold nonempty_compacts.Kuratowski_embedding, rw [rangeΨ]; refl },
id                                                                  └────┘
src             └────────────────────────────────────────────┘  └──┘        └───┘
typ             └────────────────────────────────────────────┘  └──┘└────┘  └───┘
doc             └────────────────────────────────────────────┘  └──┘        └───┘
txt             └────────────────────────────────────────────┘  └──┘        └───┘
par             └────────────────────────────────────────────┘  └──┘        └───┘
pid                    └─────────────────────────────────────┘    └┘            
st            └─────────────────────────────────────────────┘└──────────┘└─────┘└┘
101      have g := cast E f,
id                 └──┘  
src      └────────┘└──┘ 
typ      └────────┘└──┘
doc      └────────┘     
txt      └────────┘     
par      └────────┘     
pid      └────┘└─┘     
st   ─────────────────────┘└─
102      exact ⟨g⟩ }
id              
src      └────┘  └┘
typ      └────┘ └┘
doc      └────┘  └┘
txt      └────┘  └┘
par      └────┘  └┘
pid             
st   ─────────────┘└─
103  end
st   ──┘
104  
105  lemma eq_to_GH_space {p : nonempty_compacts ℓ_infty_ℝ} : ⟦p⟧ = to_GH_space p.val :=
id                             └───────────────┘ └───────┘      └─────────┘ └──┘
src                            └───────────────┘ └───────┘       └─────────┘  └──┘
typ                            └───────────────┘ └───────┘      └─────────┘ └──┘
doc                            └───────────────┘ └───────┘          └─────────┘
106  begin
st   └─────
107   refine eq_to_GH_space_iff.2 ⟨((λx, x) : p.val → ℓ_infty_ℝ), _, subtype.val_range⟩,
id           └────────────────┘               └───┘   └───────┘      └───────────────┘
src   └─────┘└────────────────┘└─┘    └─┘ └──┘└───┘ └───────┘└────┘└───────────────┘
typ   └─────┘└────────────────┘└─┘    └─┘ └──┘└───┘ └───────┘└────┘└───────────────┘
doc   └─────┘                  └─┘    └─┘ └──┘      └───────┘└────┘                 
txt   └─────┘                  └─┘    └─┘ └──┘               └────┘                 
par   └─────┘                  └─┘    └─┘ └──┘               └────┘                 
pid                           └─┘    └─┘ └──┘               └────┘                 
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
108   apply isometry_subtype_val
id          └──────────────────┘
src   └────┘└──────────────────┘
typ   └────┘└──────────────────┘
doc   └────┘└──────────────────┘
txt   └────┘                    
par   └────┘                    
pid                            
st   ───────────────────────────┘
109  end
st   └─┘
110  
111  section
112  local attribute [reducible] GH_space.rep
id                               └──────────┘
src                              └──────────┘
typ                              └──────────┘
doc                   └───────┘  └──────────┘
113  
114  instance rep_GH_space_metric_space {p : GH_space} : metric_space (p.rep) :=
id                                           └──────┘    └──────────┘  └──┘
src                                          └──────┘    └──────────┘   └──┘
typ                                          └──────┘    └──────────┘  └──┘
doc                                          └──────┘    └──────────┘   └──┘
115  by apply_instance
src     └──────────────
typ     └──────────────
doc     └──────────────
txt     └──────────────
par     └──────────────
pid                   
st     └───────────────
116  
src  
typ  
doc  
txt  
par  
pid  
st   
117  instance rep_GH_space_compact_space {p : GH_space} : compact_space (p.rep) :=
id                                            └──────┘    └───────────┘  └──┘
src                                           └──────┘    └───────────┘   └──┘
typ                                           └──────┘    └───────────┘  └──┘
doc                                           └──────┘    └───────────┘   └──┘
118  by apply_instance
src     └──────────────
typ     └──────────────
doc     └──────────────
txt     └──────────────
par     └──────────────
pid                   
st     └───────────────
119  
src  
typ  
doc  
txt  
par  
pid  
st   
120  instance rep_GH_space_nonempty {p : GH_space} : nonempty (p.rep) :=
id                                       └──────┘    └──────┘  └──┘
src                                      └──────┘    └──────┘   └──┘
typ                                      └──────┘    └──────┘  └──┘
doc                                      └──────┘               └──┘
121  by apply_instance
src     └─────────────┘
typ     └─────────────┘
doc     └─────────────┘
txt     └─────────────┘
par     └─────────────┘
pid                   
st     └──────────────┘
122  end
123  
124  lemma GH_space.to_GH_space_rep (p : GH_space) : to_GH_space (p.rep) = p :=
id                                       └──────┘    └─────────┘  └──┘   
src                                      └──────┘    └─────────┘   └──┘  
typ                                      └──────┘    └─────────┘  └──┘   
doc                                      └──────┘    └─────────┘   └──┘
125  begin
st   └─────
126    change to_GH_space (quot.out p).val = p,
id            └─────────┘  └──────┘         
src    └─────┘└─────────┘ └──────┘ └────┘
typ    └─────┘└─────────┘ └──────┘ └────┘
doc    └─────┘└─────────┘ └──────┘ └────┘ 
txt    └─────┘                     └────┘ 
par    └─────┘                     └────┘ 
pid                               └────┘ 
st   ────────────────────────────────────────┘└─
127    rw ← eq_to_GH_space,
id          └────────────┘
src    └───┘└────────────┘
typ    └───┘└────────────┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ────────────────────┘└─
128    exact quot.out_eq p
id           └─────────┘ 
src    └────┘└─────────┘ 
typ    └────┘└─────────┘
doc    └────┘            
txt    └────┘            
par    └────┘            
pid                     
st   ─────────────────────┘
129  end
st   └─┘
130  
131  /-- Two nonempty compact spaces have the same image in `GH_space` if and only if they are isometric -/
132  lemma to_GH_space_eq_to_GH_space_iff_isometric {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id                                                                └──────────┘    └───────────┘    └──────┘ 
src                                                               └──────────┘     └───────────┘     └──────┘
typ                                                               └──────────┘    └───────────┘    └──────┘ 
doc                                                               └──────────┘     └───────────┘
133    {β : Type u} [metric_space β] [compact_space β] [nonempty β] :
id                   └──────────┘    └───────────┘    └──────┘ 
src                  └──────────┘     └───────────┘     └──────┘
typ                  └──────────┘    └───────────┘    └──────┘ 
doc                  └──────────┘     └───────────┘
134    to_GH_space α = to_GH_space β ↔ nonempty (α ≃ᵢ β) :=
id     └─────────┘   └─────────┘   └──────┘   └┘ 
src    └─────────┘    └─────────┘    └──────┘    └┘
typ    └─────────┘   └─────────┘   └──────┘   └┘ 
doc    └─────────┘     └─────────┘                 └┘
135  ⟨begin
st    └─────
136    simp only [to_GH_space, quotient.eq],
id                └─────────┘  └─────────┘
src    └─────────┘└─────────┘└┘└─────────┘
typ    └─────────┘└─────────┘└┘└─────────┘
doc    └─────────┘└─────────┘└┘           
txt    └─────────┘           └┘           
par    └─────────┘           └┘           
pid        └──┘└┘           └┘           
st   ─────────────────────────────────────┘└─
137    assume h,
src    └──────┘
typ    └──────┘
doc    └──────┘
txt    └──────┘
par    └──────┘
pid    └──────┘
st   ─────────┘└─
138    rcases h with e,
id            
src    └─────┘ └─────┘
typ    └─────┘└─────┘
doc    └─────┘ └─────┘
txt    └─────┘ └─────┘
par    └─────┘ └─────┘
pid           └─────┘
st   ────────────────┘└─
139    have I : ((nonempty_compacts.Kuratowski_embedding α).val ≃ᵢ (nonempty_compacts.Kuratowski_embedding β).val)
id                                                              └┘  └────────────────────────────────────┘
src    └───────┘                                         └────┘└┘ └────────────────────────────────────┘ └──────
typ    └───────┘                                         └────┘└┘ └────────────────────────────────────┘ └──────
doc    └───────┘                                         └────┘└┘ └────────────────────────────────────┘ └──────
txt    └───────┘                                         └────┘                                          └──────
par    └───────┘                                         └────┘                                          └──────
pid    └────┘└─┘                                         └────┘                                          └──────
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────
140            = ((range (Kuratowski_embedding α)) ≃ᵢ (range (Kuratowski_embedding β))),
id                                                   └───┘  └──────────────────┘ 
src  ─────────┘                             └─┘   └───┘ └──────────────────┘ └─┘
typ  ─────────┘                            └─┘   └───┘ └──────────────────┘└─┘
doc  ─────────┘                              └─┘   └───┘ └──────────────────┘ └─┘
txt  ─────────┘                              └─┘                              └─┘
par  ─────────┘                              └─┘                              └─┘
pid  ─────────┘                              └─┘                              └─┘
st   ─────────────────────────────────────────────────────────────────────────────────┘
141      by { dunfold nonempty_compacts.Kuratowski_embedding, refl },
src           └────────────────────────────────────────────┘  └───┘
typ           └────────────────────────────────────────────┘  └───┘
doc           └────────────────────────────────────────────┘  └───┘
txt           └────────────────────────────────────────────┘  └───┘
par           └────────────────────────────────────────────┘  └───┘
pid                  └─────────────────────────────────────┘      
st          └─────────────────────────────────────────────┘└─────┘└┘
142    have e' := cast I e,
id                └──┘  
src    └─────────┘└──┘ 
typ    └─────────┘└──┘
doc    └─────────┘     
txt    └─────────┘     
par    └─────────┘     
pid    └─────┘└─┘     
st   ────────────────────┘└─
143    have f := (Kuratowski_embedding.isometry α).isometric_on_range,
id                └───────────────────────────┘ 
src    └────────┘ └───────────────────────────┘ └──────────────────┘
typ    └────────┘ └───────────────────────────┘└──────────────────┘
doc    └────────┘ └───────────────────────────┘ └──────────────────┘
txt    └────────┘                               └──────────────────┘
par    └────────┘                               └──────────────────┘
pid    └────┘└─┘                               └─────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
144    have g := (Kuratowski_embedding.isometry β).isometric_on_range.symm,
id                └───────────────────────────┘ 
src    └────────┘ └───────────────────────────┘ └───────────────────────┘
typ    └────────┘ └───────────────────────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────────┘ └───────────────────────┘
txt    └────────┘                               └───────────────────────┘
par    └────────┘                               └───────────────────────┘
pid    └────┘└─┘                               └──────────────────────┘
st   ────────────────────────────────────────────────────────────────────┘└─
145    have h := (f.trans e').trans g,
id                └─────┘ └┘        
src    └────────┘ └─────┘  └──────┘
typ    └────────┘ └─────┘└┘└──────┘
doc    └────────┘ └─────┘  └──────┘
txt    └────────┘          └──────┘
par    └────────┘          └──────┘
pid    └────┘└─┘          └──────┘
st   ───────────────────────────────┘└─
146    exact ⟨h⟩
id            
src    └────┘  └┘
typ    └────┘ └┘
doc    └────┘  └┘
txt    └────┘  └┘
par    └────┘  └┘
pid           
st   ───────────┘
147  end,
st   └─┘
148  begin
st   └─────
149    rintros ⟨e⟩,
src    └─────────┘
typ    └─────────┘
doc    └─────────┘
txt    └─────────┘
par    └─────────┘
pid           └──┘
st   ────────────┘└─
150    simp only [to_GH_space, quotient.eq],
id                └─────────┘  └─────────┘
src    └─────────┘└─────────┘└┘└─────────┘
typ    └─────────┘└─────────┘└┘└─────────┘
doc    └─────────┘└─────────┘└┘           
txt    └─────────┘           └┘           
par    └─────────┘           └┘           
pid        └──┘└┘           └┘           
st   ─────────────────────────────────────┘└─
151    have f := (Kuratowski_embedding.isometry α).isometric_on_range.symm,
id                └───────────────────────────┘ 
src    └────────┘ └───────────────────────────┘ └───────────────────────┘
typ    └────────┘ └───────────────────────────┘└───────────────────────┘
doc    └────────┘ └───────────────────────────┘ └───────────────────────┘
txt    └────────┘                               └───────────────────────┘
par    └────────┘                               └───────────────────────┘
pid    └────┘└─┘                               └──────────────────────┘
st   ────────────────────────────────────────────────────────────────────┘└─
152    have g := (Kuratowski_embedding.isometry β).isometric_on_range,
id                └───────────────────────────┘ 
src    └────────┘ └───────────────────────────┘ └──────────────────┘
typ    └────────┘ └───────────────────────────┘└──────────────────┘
doc    └────────┘ └───────────────────────────┘ └──────────────────┘
txt    └────────┘                               └──────────────────┘
par    └────────┘                               └──────────────────┘
pid    └────┘└─┘                               └─────────────────┘
st   ───────────────────────────────────────────────────────────────┘└─
153    have h := (f.trans e).trans g,
id                └─────┘         
src    └────────┘ └─────┘ └──────┘
typ    └────────┘ └─────┘└──────┘
doc    └────────┘ └─────┘ └──────┘
txt    └────────┘         └──────┘
par    └────────┘         └──────┘
pid    └────┘└─┘         └──────┘
st   ──────────────────────────────┘└─
154    have I : ((range (Kuratowski_embedding α)) ≃ᵢ (range (Kuratowski_embedding β))) =
id                                                    └───┘  └──────────────────┘
src    └───────┘                             └─┘   └───┘ └──────────────────┘ └──┘ 
typ    └───────┘                             └─┘   └───┘ └──────────────────┘ └──┘ 
doc    └───────┘                             └─┘   └───┘ └──────────────────┘ └──┘ 
txt    └───────┘                             └─┘                              └──┘ 
par    └───────┘                             └─┘                              └──┘ 
pid    └────┘└─┘                             └─┘                              └──┘ 
st   ────────────────────────────────────────────────────────────────────────────────────
155      ((nonempty_compacts.Kuratowski_embedding α).val ≃ᵢ (nonempty_compacts.Kuratowski_embedding β).val),
id                                                          └────────────────────────────────────┘ 
src  ───┘                                         └────┘   └────────────────────────────────────┘ └────┘
typ  ───┘                                        └────┘   └────────────────────────────────────┘└────┘
doc  ───┘                                         └────┘   └────────────────────────────────────┘ └────┘
txt  ───┘                                         └────┘                                          └────┘
par  ───┘                                         └────┘                                          └────┘
pid  ───┘                                         └────┘                                          └────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────┘
156      by { dunfold nonempty_compacts.Kuratowski_embedding, refl },
src           └────────────────────────────────────────────┘  └───┘
typ           └────────────────────────────────────────────┘  └───┘
doc           └────────────────────────────────────────────┘  └───┘
txt           └────────────────────────────────────────────┘  └───┘
par           └────────────────────────────────────────────┘  └───┘
pid                  └─────────────────────────────────────┘      
st          └─────────────────────────────────────────────┘└─────┘└┘
157    have h' := cast I h,
id                └──┘  
src    └─────────┘└──┘ 
typ    └─────────┘└──┘
doc    └─────────┘     
txt    └─────────┘     
par    └─────────┘     
pid    └─────┘└─┘     
st   ────────────────────┘└─
158    exact ⟨h'⟩
id            └┘
src    └────┘   └┘
typ    └────┘ └┘└┘
doc    └────┘   └┘
txt    └────┘   └┘
par    └────┘   └┘
pid            
st   ────────────┘
159  end⟩
st   └─┘
160  
161  /-- Distance on `GH_space`: the distance between two nonempty compact spaces is the infimum
162  Hausdorff distance between isometric copies of the two spaces in a metric space. For the definition,
163  we only consider embeddings in `ℓ^∞(ℝ)`, but we will prove below that it works for all spaces. -/
164  instance : has_dist (GH_space) :=
id              └──────┘  └──────┘
src             └──────┘  └──────┘
typ             └──────┘  └──────┘
doc             └──────┘  └──────┘
165  { dist := λx y, Inf ((λp : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ, Hausdorff_dist p.1.val p.2.val) ''
id                 └─┘        └───────────────┘ └───────┘  └───────────────┘ └───────┘  └────────────┘  └─┘   └─┘   └┘
src                  └─┘        └───────────────┘ └───────┘  └───────────────┘ └───────┘  └────────────┘   └─┘    └─┘   └┘
typ                └─┘        └───────────────┘ └───────┘  └───────────────┘ └───────┘  └────────────┘  └─┘   └─┘   └┘
doc                  └─┘        └───────────────┘ └───────┘   └───────────────┘ └───────┘  └────────────┘
166                        (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y})) }
id                          └──────┘             
src                         └──────┘                 
typ                         └──────┘             
doc                         └──────┘
167  
168  /-- The Gromov-Hausdorff distance between two nonempty compact metric spaces, equal by definition to
169  the distance of the equivalence classes of these spaces in the Gromov-Hausdorff space. -/
170  def GH_dist (α : Type u) (β : Type v) [metric_space α] [nonempty α] [compact_space α]
id                                          └──────────┘    └──────┘    └───────────┘ 
src                                         └──────────┘     └──────┘     └───────────┘
typ                                         └──────────┘    └──────┘    └───────────┘ 
doc                                         └──────────┘                  └───────────┘
171    [metric_space β] [nonempty β] [compact_space β] : ℝ := dist (to_GH_space α) (to_GH_space β)
id      └──────────┘    └──────┘    └───────────┘         └──┘  └─────────┘    └─────────┘ 
src     └──────────┘     └──────┘     └───────────┘          └──┘  └─────────┘     └─────────┘
typ     └──────────┘    └──────┘    └───────────┘         └──┘  └─────────┘    └─────────┘ 
doc     └──────────┘                  └───────────┘                 └─────────┘     └─────────┘
172  
173  lemma dist_GH_dist (p q : GH_space) : dist p q = GH_dist (p.rep) (q.rep) :=
id                             └──────┘    └──┘    └─────┘  └──┘   └──┘
src                            └──────┘    └──┘      └─────┘   └──┘    └──┘
typ                            └──────┘    └──┘    └─────┘  └──┘   └──┘
doc                            └──────┘               └─────┘   └──┘    └──┘
174  by rw [GH_dist, p.to_GH_space_rep, q.to_GH_space_rep]
id          └─────┘
src     └──┘└─────┘└┘                 └┘                 └─
typ     └──┘└─────┘└┘└───────────────┘└┘└───────────────┘└─
doc     └──┘└─────┘└┘                 └┘                 └─
txt     └──┘       └┘                 └┘                 └─
par     └──┘       └┘                 └┘                 └─
pid       └┘       └┘                 └┘                 
st     └──────────┘└─────────────────┘└─────────────────┘
175  
src  
typ  
doc  
txt  
par  
pid  
st   
176  /-- The Gromov-Hausdorff distance between two spaces is bounded by the Hausdorff distance
177  of isometric copies of the spaces, in any metric space. -/
178  theorem GH_dist_le_Hausdorff_dist {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id                                                   └──────────┘    └───────────┘    └──────┘ 
src                                                  └──────────┘     └───────────┘     └──────┘
typ                                                  └──────────┘    └───────────┘    └──────┘ 
doc                                                  └──────────┘     └───────────┘
179    {β : Type v} [metric_space β] [compact_space β] [nonempty β]
id                   └──────────┘    └───────────┘    └──────┘ 
src                  └──────────┘     └───────────┘     └──────┘
typ                  └──────────┘    └───────────┘    └──────┘ 
doc                  └──────────┘     └───────────┘
180    {γ : Type w} [metric_space γ] {Φ : α → γ} {Ψ : β → γ} (ha : isometry Φ) (hb : isometry Ψ) :
id                   └──────────┘                             └──────┘         └──────┘ 
src                  └──────────┘                                  └──────┘          └──────┘
typ                  └──────────┘                             └──────┘         └──────┘ 
doc                  └──────────┘                                  └──────┘          └──────┘
181    GH_dist α β ≤ Hausdorff_dist (range Φ) (range Ψ) :=
id     └─────┘    └────────────┘  └───┘    └───┘ 
src    └─────┘      └────────────┘  └───┘     └───┘
typ    └─────┘    └────────────┘  └───┘    └───┘ 
doc    └─────┘       └────────────┘  └───┘     └───┘
182  begin
st   └─────
183    /- For the proof, we want to embed `γ` in `ℓ^∞(ℝ)`, to say that the Hausdorff distance is realized
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────
184    in `ℓ^∞(ℝ)` and therefore bounded below by the Gromov-Hausdorff-distance. However, `γ` is not
st   ────────────────────────────────────────────────────────────────────────────────────────────────
185    separable in general. We restrict to the union of the images of `α` and `β` in `γ`, which is
st   ───────────────────────────────────────────────────────────────────────────────────────────────
186    separable and therefore embeddable in `ℓ^∞(ℝ)`. -/
st   ─────────────────────────────────────────────────────
187    rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id            └────────────────────┘ 
src    └─────┘└────────────────────┘ └───────────┘
typ    └─────┘└────────────────────┘└───────────┘
doc    └─────┘                       └───────────┘
txt    └─────┘                       └───────────┘
par    └─────┘                       └───────────┘
pid                                 └───────────┘
st   ─────────────────────────────────────────────┘└─
188    letI : inhabited α := ⟨xα⟩,
id            └───────┘      └┘
src    └─────┘└───────┘ └──┘   
typ    └─────┘└───────┘└──┘ └┘
doc    └─────┘          └──┘   
txt    └─────┘          └──┘   
par    └─────┘          └──┘   
pid        └┘          └──┘   
st   ───────────────────────────┘└─
189    letI : inhabited β := classical.inhabited_of_nonempty (by assumption),
id            └───────┘     └─────────────────────────────┘
src    └─────┘└───────┘ └──┘└─────────────────────────────┘   └────────┘
typ    └─────┘└───────┘└──┘└─────────────────────────────┘   └────────┘
doc    └─────┘          └──┘                                  └────────┘
txt    └─────┘          └──┘                                  └────────┘
par    └─────┘          └──┘                                  └────────┘
pid        └┘          └──┘                                  └──────────┘
st   ──────────────────────────────────────────────────────────┘└─────────┘└─
190    let s : set γ := (range Φ) ∪ (range Ψ),
id             └─┘                └───┘ 
src    └──────┘└─┘ └──┘       └┘ └───┘ 
typ    └──────┘└─┘└──┘      └┘ └───┘
doc    └──────┘    └──┘       └┘  └───┘ 
txt    └──────┘    └──┘       └┘        
par    └──────┘    └──┘       └┘        
pid    └───┘└─┘    └──┘       └┘        
st   ───────────────────────────────────────┘└─
191    let Φ' : α → subtype s := λy, ⟨Φ y, mem_union_left _ (mem_range_self _)⟩,
id                 └─────┘              └────────────┘    └────────────┘
src    └───────┘  └─────┘ └──┘ └─┘   └┘└────────────┘└─┘ └────────────┘└──┘
typ    └───────┘ └─────┘└──┘ └─┘  └┘└────────────┘└─┘ └────────────┘└──┘
doc    └───────┘          └──┘ └─┘   └┘              └─┘               └──┘
txt    └───────┘          └──┘ └─┘   └┘              └─┘               └──┘
par    └───────┘          └──┘ └─┘   └┘              └─┘               └──┘
pid    └────┘└─┘          └──┘ └─┘   └┘              └─┘               └──┘
st   ─────────────────────────────────────────────────────────────────────────┘└─
192    let Ψ' : β → subtype s := λy, ⟨Ψ y, mem_union_right _ (mem_range_self _)⟩,
id                 └─────┘              └─────────────┘    └────────────┘
src    └───────┘  └─────┘ └──┘ └─┘   └┘└─────────────┘└─┘ └────────────┘└──┘
typ    └───────┘ └─────┘└──┘ └─┘  └┘└─────────────┘└─┘ └────────────┘└──┘
doc    └───────┘          └──┘ └─┘   └┘               └─┘               └──┘
txt    └───────┘          └──┘ └─┘   └┘               └─┘               └──┘
par    └───────┘          └──┘ └─┘   └┘               └─┘               └──┘
pid    └────┘└─┘          └──┘ └─┘   └┘               └─┘               └──┘
st   ──────────────────────────────────────────────────────────────────────────┘└─
193    have IΦ' : isometry Φ' := λx y, ha x y,
id                └──────┘ └┘          └┘
src    └─────────┘└──────┘  └──┘ └───┘   
typ    └─────────┘└──────┘└┘└──┘ └───┘└┘ 
doc    └─────────┘└──────┘  └──┘ └───┘   
txt    └─────────┘          └──┘ └───┘   
par    └─────────┘          └──┘ └───┘   
pid    └──────┘└─┘          └──┘ └───┘   
st   ───────────────────────────────────────┘└─
194    have IΨ' : isometry Ψ' := λx y, hb x y,
id                └──────┘ └┘          └┘
src    └─────────┘└──────┘  └──┘ └───┘   
typ    └─────────┘└──────┘└┘└──┘ └───┘└┘ 
doc    └─────────┘└──────┘  └──┘ └───┘   
txt    └─────────┘          └──┘ └───┘   
par    └─────────┘          └──┘ └───┘   
pid    └──────┘└─┘          └──┘ └───┘   
st   ───────────────────────────────────────┘└─
195    have : compact s, from (compact_range ha.continuous).union (compact_range hb.continuous),
id            └─────┘                       └───────────┘         └───────────┘ └───────────┘
src    └─────┘└─────┘   └───┘              └───────────┘└──────┘ └───────────┘└───────────┘
typ    └─────┘└─────┘  └───┘              └───────────┘└──────┘ └───────────┘└───────────┘
doc    └─────┘└─────┘   └───┘              └───────────┘└──────┘              └───────────┘
txt    └─────┘          └───┘                           └──────┘                           
par    └─────┘          └───┘                           └──────┘                           
pid    └───┘└┘          └───┘                           └──────┘                           
st   ─────────────────┘└──────────────────────────────────────────────────────────────────────┘└─
196    letI : metric_space (subtype s) := by apply_instance,
id            └──────────┘  └─────┘ 
src    └─────┘└──────────┘ └─────┘ └───┘  └────────────┘
typ    └─────┘└──────────┘ └─────┘└───┘  └────────────┘
doc    └─────┘└──────────┘         └───┘  └────────────┘
txt    └─────┘                     └───┘  └────────────┘
par    └─────┘                     └───┘  └────────────┘
pid        └┘                     └──┘  └─────────────┘
st   ──────────────────────────────────────┘└─────────────┘└─
197    haveI : compact_space (subtype s) := ⟨compact_iff_compact_univ.1 ‹compact s›⟩,
id             └───────────┘  └─────┘       └──────────────────────┘   └─────┘ 
src    └──────┘└───────────┘ └─────┘ └───┘ └──────────────────────┘└─┘└─────┘ 
typ    └──────┘└───────────┘ └─────┘└───┘ └──────────────────────┘└─┘└─────┘
doc    └──────┘└───────────┘         └───┘                         └─┘└─────┘ 
txt    └──────┘                      └───┘                         └─┘          
par    └──────┘                      └───┘                         └─┘          
pid         └┘                      └──┘                         └─┘          
st   ──────────────────────────────────────────────────────────────────────────────┘└─
198    haveI : nonempty (subtype s) := ⟨Φ' xα⟩,
id             └──────┘  └─────┘       └┘ └┘
src    └──────┘└──────┘ └─────┘ └───┘     
typ    └──────┘└──────┘ └─────┘└───┘ └┘└┘
doc    └──────┘                 └───┘     
txt    └──────┘                 └───┘     
par    └──────┘                 └───┘     
pid         └┘                 └──┘     
st   ────────────────────────────────────────┘└─
199    have ΦΦ' : Φ = subtype.val ∘ Φ', by { funext, refl },
id                  └─────────┘  └┘
src    └─────────┘ └─────────┘         └────┘  └───┘
typ    └─────────┘└─────────┘└┘       └────┘  └───┘
doc    └─────────┘                       └────┘  └───┘
txt    └─────────┘                       └────┘  └───┘
par    └─────────┘                       └────┘  └───┘
pid    └──────┘└─┘                                   
st   ────────────────────────────────┘     └─────┘└─────┘└┘
200    have ΨΨ' : Ψ = subtype.val ∘ Ψ', by { funext, refl },
id                   └─────────┘   └┘
src    └─────────┘  └─────────┘          └────┘  └───┘
typ    └─────────┘ └─────────┘ └┘       └────┘  └───┘
doc    └─────────┘                       └────┘  └───┘
txt    └─────────┘                       └────┘  └───┘
par    └─────────┘                       └────┘  └───┘
pid    └──────┘└─┘                                   
st   ────────────────────────────────┘     └─────┘└─────┘└┘
201    have : Hausdorff_dist (range Φ) (range Ψ) = Hausdorff_dist (range Φ') (range Ψ'),
id                                               └────────────┘        └┘   └───┘ └┘
src    └─────┘                     └┘       └┘ └────────────┘        └┘ └───┘  
typ    └─────┘                    └┘      └┘ └────────────┘      └┘└┘ └───┘└┘
doc    └─────┘                     └┘       └┘ └────────────┘        └┘ └───┘  
txt    └─────┘                     └┘       └┘                       └┘        
par    └─────┘                     └┘       └┘                       └┘        
pid    └───┘└┘                     └┘       └┘                       └┘        
st   ─────────────────────────────────────────────────────────────────────────────────┘└─
202    { rw [ΦΦ', ΨΨ', range_comp, range_comp],
id           └─┘  └─┘  └────────┘  └────────┘
src      └──┘   └┘   └┘└────────┘└┘└────────┘
typ      └──┘└─┘└┘└─┘└┘└────────┘└┘└────────┘
doc      └──┘   └┘   └┘          └┘          
txt      └──┘   └┘   └┘          └┘          
par      └──┘   └┘   └┘          └┘          
pid        └┘   └┘   └┘          └┘          
st   ───┘└─────┘└───┘└──────────┘└──────────┘└──
203      exact Hausdorff_dist_image (isometry_subtype_val) },
id             └──────────────────┘  └──────────────────┘
src      └────┘└──────────────────┘ └──────────────────┘└┘
typ      └────┘└──────────────────┘ └──────────────────┘└┘
doc      └────┘└──────────────────┘ └──────────────────┘└┘
txt      └────┘                                         └┘
par      └────┘                                         └┘
pid                                                    
st   ─────────────────────────────────────────────────────┘└┘
204    rw this,
id        └──┘
src    └─┘
typ    └─┘└──┘
doc    └─┘
txt    └─┘
par    └─┘
pid      
st   ────────┘└─
205    -- Embed `s` in `ℓ^∞(ℝ)` through its Kuratowski embedding
st   ────────────────────────────────────────────────────────────
206    let F := Kuratowski_embedding (subtype s),
id              └──────────────────┘  └─────┘ 
src    └───────┘└──────────────────┘ └─────┘ 
typ    └───────┘└──────────────────┘ └─────┘
doc    └───────┘└──────────────────┘         
txt    └───────┘                             
par    └───────┘                             
pid    └───┘└─┘                             
st   ──────────────────────────────────────────┘└─
207    have : Hausdorff_dist (F '' (range Φ')) (F '' (range Ψ')) = Hausdorff_dist (range Φ') (range Ψ') :=
id                              └┘                                └────────────┘        └┘   └───┘ └┘
src    └─────┘                └┘        └─┘            └─┘ └────────────┘        └┘ └───┘  └────
typ    └─────┘                └┘        └─┘           └─┘ └────────────┘      └┘└┘ └───┘└┘└────
doc    └─────┘                          └─┘            └─┘ └────────────┘        └┘ └───┘  └────
txt    └─────┘                          └─┘            └─┘                       └┘        └────
par    └─────┘                          └─┘            └─┘                       └┘        └────
pid    └───┘└┘                          └─┘            └─┘                       └┘        └───
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────
208      Hausdorff_dist_image (Kuratowski_embedding.isometry _),
id       └──────────────────┘  └───────────────────────────┘
src  ───┘└──────────────────┘ └───────────────────────────┘└─┘
typ  ───┘└──────────────────┘ └───────────────────────────┘└─┘
doc  ───┘└──────────────────┘ └───────────────────────────┘└─┘
txt  ───┘                                                  └─┘
par  ───┘                                                  └─┘
pid  ───┘                                                  └─┘
st   ─────────────────────────────────────────────────────────┘└─
209    rw ← this,
id          └──┘
src    └───┘
typ    └───┘└──┘
doc    └───┘
txt    └───┘
par    └───┘
pid      └─┘
st   ──────────┘└─
210    -- Let `A` and `B` be the images of `α` and `β` under this embedding. They are in `ℓ^∞(ℝ)`, and
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
211    -- their Hausdorff distance is the same as in the original space.
st   ────────────────────────────────────────────────────────────────────
212    let A : nonempty_compacts ℓ_infty_ℝ := ⟨F '' (range Φ'), ⟨(range_nonempty _).image _,
id             └───────────────┘ └───────┘          └───┘ └┘     └────────────┘
src    └──────┘└───────────────┘└───────┘└──┘     └───┘  └─┘  └────────────┘└────────────
typ    └──────┘└───────────────┘└───────┘└──┘    └───┘└┘└─┘  └────────────┘└────────────
doc    └──────┘└───────────────┘└───────┘└──┘     └───┘  └─┘                └────────────
txt    └──────┘                          └──┘            └─┘                └────────────
par    └──────┘                          └──┘            └─┘                └────────────
pid    └───┘└─┘                          └──┘            └─┘                └────────────
st   ────────────────────────────────────────────────────────────────────────────────────────
213        (compact_range IΦ'.continuous).image (Kuratowski_embedding.isometry _).continuous⟩⟩,
id          └───────────┘ └────────────┘         └───────────────────────────┘
src  ─────┘ └───────────┘└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
typ  ─────┘ └───────────┘└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
doc  ─────┘              └────────────┘└──────┘ └───────────────────────────┘└──────────────┘
txt  ─────┘                            └──────┘                              └──────────────┘
par  ─────┘                            └──────┘                              └──────────────┘
pid  ─────┘                            └──────┘                              └──────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
214    let B : nonempty_compacts ℓ_infty_ℝ := ⟨F '' (range Ψ'), ⟨(range_nonempty _).image _,
id             └───────────────┘ └───────┘          └───┘ └┘     └────────────┘
src    └──────┘└───────────────┘└───────┘└──┘     └───┘  └─┘  └────────────┘└────────────
typ    └──────┘└───────────────┘└───────┘└──┘    └───┘└┘└─┘  └────────────┘└────────────
doc    └──────┘└───────────────┘└───────┘└──┘     └───┘  └─┘                └────────────
txt    └──────┘                          └──┘            └─┘                └────────────
par    └──────┘                          └──┘            └─┘                └────────────
pid    └───┘└─┘                          └──┘            └─┘                └────────────
st   ────────────────────────────────────────────────────────────────────────────────────────
215        (compact_range IΨ'.continuous).image (Kuratowski_embedding.isometry _).continuous⟩⟩,
id          └───────────┘ └────────────┘         └───────────────────────────┘
src  ─────┘ └───────────┘└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
typ  ─────┘ └───────────┘└────────────┘└──────┘ └───────────────────────────┘└──────────────┘
doc  ─────┘              └────────────┘└──────┘ └───────────────────────────┘└──────────────┘
txt  ─────┘                            └──────┘                              └──────────────┘
par  ─────┘                            └──────┘                              └──────────────┘
pid  ─────┘                            └──────┘                              └──────────────┘
st   ────────────────────────────────────────────────────────────────────────────────────────┘└─
216    have Aα : ⟦A⟧ = to_GH_space α,
id                  └─────────┘ 
src    └────────┘  └─────────┘
typ    └────────┘ └─────────┘
doc    └────────┘    └─────────┘
txt    └────────┘               
par    └────────┘               
pid    └─────┘└─┘               
st   ──────────────────────────────┘└─
217    { rw eq_to_GH_space_iff,
id          └────────────────┘
src      └─┘└────────────────┘
typ      └─┘└────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└───────────────────┘└─
218      exact ⟨λx, F (Φ' x), ⟨(Kuratowski_embedding.isometry _).comp IΦ', by rw range_comp⟩⟩ },
id                    └┘       └───────────────────────────┘         └─┘        └────────┘
src      └────┘  └─┘     └─┘  └───────────────────────────┘└───────┘   └┘  └─┘└────────┘└─┘
typ      └────┘  └─┘ └┘ └─┘  └───────────────────────────┘└───────┘└─┘└┘  └─┘└────────┘└─┘
doc      └────┘  └─┘     └─┘  └───────────────────────────┘└───────┘   └┘  └─┘          └─┘
txt      └────┘  └─┘     └─┘                               └───────┘   └┘  └─┘          └─┘
par      └────┘  └─┘     └─┘                               └───────┘   └┘  └─┘          └─┘
pid             └─┘     └─┘                               └───────┘   └┘  └──┘          └┘
st   ───────────────────────────────────────────────────────────────────────┘└────────────┘└─┘└┘
219    have Bβ : ⟦B⟧ = to_GH_space β,
id                    └─────────┘ 
src    └────────┘    └─────────┘
typ    └────────┘   └─────────┘
doc    └────────┘    └─────────┘
txt    └────────┘               
par    └────────┘               
pid    └─────┘└─┘               
st   ──────────────────────────────┘└─
220    { rw eq_to_GH_space_iff,
id          └────────────────┘
src      └─┘└────────────────┘
typ      └─┘└────────────────┘
doc      └─┘
txt      └─┘
par      └─┘
pid        
st   ───┘└───────────────────┘└─
221      exact ⟨λx, F (Ψ' x), ⟨(Kuratowski_embedding.isometry _).comp IΨ', by rw range_comp⟩⟩ },
id                    └┘       └───────────────────────────┘         └─┘        └────────┘
src      └────┘  └─┘     └─┘  └───────────────────────────┘└───────┘   └┘  └─┘└────────┘└─┘
typ      └────┘  └─┘ └┘ └─┘  └───────────────────────────┘└───────┘└─┘└┘  └─┘└────────┘└─┘
doc      └────┘  └─┘     └─┘  └───────────────────────────┘└───────┘   └┘  └─┘          └─┘
txt      └────┘  └─┘     └─┘                               └───────┘   └┘  └─┘          └─┘
par      └────┘  └─┘     └─┘                               └───────┘   └┘  └─┘          └─┘
pid             └─┘     └─┘                               └───────┘   └┘  └──┘          └┘
st   ───────────────────────────────────────────────────────────────────────┘└────────────┘└─┘└┘
222    refine cInf_le ⟨0,
id            └─────┘
src    └─────┘└─────┘ └──
typ    └─────┘└─────┘ └──
doc    └─────┘        └──
txt    └─────┘        └──
par    └─────┘        └──
pid                  └──
st   ─────────────────────
223      begin simp [lower_bounds], assume t _ _ _ _ ht, rw ← ht, exact Hausdorff_dist_nonneg end⟩ _,
id                   └──────────┘                             └┘        └───────────────────┘
src  ───┘     └────┘└──────────┘└┘└─────────────────┘└┘└───┘  └┘└────┘└───────────────────┘└────┘
typ  ───┘     └────┘└──────────┘└┘└─────────────────┘└┘└───┘└┘└──────┘└───────────────────┘└─────┘
doc  ───┘     └────┘└──────────┘└┘└─────────────────┘└┘└───┘  └┘└────┘└───────────────────┘└────┘
txt  ───┘     └────┘            └┘└─────────────────┘└┘└───┘  └┘└────┘                     └────┘
par  ───┘     └────┘            └┘└─────────────────┘└┘└───┘  └──────┘                     └─────┘
pid  ───┘     └─────┘            └───────────────────────────┘  └──────┘                     └─────┘
st   ───┘└───────────────────────┘└───────────────────┘└───────┘└────────────────────────────┘└─┘└─┘└─
224    apply (mem_image _ _ _).2,
id            └───────┘
src    └────┘ └───────┘└───────┘
typ    └────┘ └───────┘└───────┘
doc    └────┘          └───────┘
txt    └────┘          └───────┘
par    └────┘          └───────┘
pid                   └─────┘└┘
st   ──────────────────────────┘└─
225    existsi (⟨A, B⟩ : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
id                                                  └───────────────┘ └───────┘
src    └──────┘   └┘ └──┘                          └───────────────┘└───────┘
typ    └──────┘  └┘└──┘                          └───────────────┘└───────┘
doc    └──────┘   └┘ └──┘                           └───────────────┘└───────┘
txt    └──────┘   └┘ └──┘                                                     
par    └──────┘   └┘ └──┘                                                     
pid              └┘ └──┘                                                     
st   ─────────────────────────────────────────────────────────────────────────────┘└─
226    simp [Aα, Bβ]
id           └┘  └┘
src    └────┘  └┘  └┘
typ    └────┘└┘└┘└┘└┘
doc    └────┘  └┘  └┘
txt    └────┘  └┘  └┘
par    └────┘  └┘  └┘
pid          └┘  
st   ───────────────┘
227  end
st   └─┘
228  
229  local attribute [instance, priority 10] inhabited_of_nonempty'
id                                           └────────────────────┘
src                                          └────────────────────┘
typ                                          └────────────────────┘
230  
231  /-- The optimal coupling constructed above realizes exactly the Gromov-Hausdorff distance,
232  essentially by design. -/
233  lemma Hausdorff_dist_optimal {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id                                              └──────────┘    └───────────┘    └──────┘ 
src                                             └──────────┘     └───────────┘     └──────┘
typ                                             └──────────┘    └───────────┘    └──────┘ 
doc                                             └──────────┘     └───────────┘
234    {β : Type v} [metric_space β] [compact_space β] [nonempty β] :
id                   └──────────┘    └───────────┘    └──────┘ 
src                  └──────────┘     └───────────┘     └──────┘
typ                  └──────────┘    └───────────┘    └──────┘ 
doc                  └──────────┘     └───────────┘
235    Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) = GH_dist α β :=
id     └────────────┘  └───┘  └─────────────┘      └───┘  └─────────────┘      └─────┘  
src    └────────────┘  └───┘  └─────────────┘        └───┘  └─────────────┘        └─────┘
typ    └────────────┘  └───┘  └─────────────┘      └───┘  └─────────────┘      └─────┘  
doc    └────────────┘  └───┘  └─────────────┘        └───┘  └─────────────┘         └─────┘
236  begin
st   └─────
237    /- we only need to check the inequality `≤`, as the other one follows from the previous lemma.
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
238       As the Gromov-Hausdorff distance is an infimum, we need to check that the Hausdorff distance
st   ──────────────────────────────────────────────────────────────────────────────────────────────────
239       in the optimal coupling is smaller than the Hausdorff distance of any coupling.
st   ─────────────────────────────────────────────────────────────────────────────────────
240       First, we check this for couplings which already have small Hausdorff distance: in this
st   ─────────────────────────────────────────────────────────────────────────────────────────────
241       case, the induced "distance" on `α ⊕ β` belongs to the candidates family introduced in the
st   ────────────────────────────────────────────────────────────────────────────────────────────────
242       definition of the optimal coupling, and the conclusion follows from the optimality
st   ────────────────────────────────────────────────────────────────────────────────────────
243       of the optimal coupling within this family.
st   ─────────────────────────────────────────────────
244    -/
st   ─────
245    have A : ∀p q : nonempty_compacts (ℓ_infty_ℝ), ⟦p⟧ = to_GH_space α → ⟦q⟧ = to_GH_space β →
id                     └───────────────┘  └───────┘                           └─────────┘
src    └───────┘ └────┘└───────────────┘ └───────┘                   └─────────┘  
typ    └───────┘ └────┘└───────────────┘ └───────┘                  └─────────┘  
doc    └───────┘ └────┘└───────────────┘ └───────┘                      └─────────┘  
txt    └───────┘ └────┘                                                              
par    └───────┘ └────┘                                                              
pid    └────┘└─┘ └────┘                                                              
st   ─────────────────────────────────────────────────────────────────────────────────────────────
246          Hausdorff_dist (p.val) (q.val) < diam (univ : set α) + 1 + diam (univ : set β) →
id                            └──┘    └──┘                            └──┘  └──┘   └─┘
src  ───────┘                └──┘└┘  └──┘└┘         └─┘    └┘└─┘ └──┘ └──┘└─┘└─┘ └┘ 
typ  ───────┘                └──┘└┘  └──┘└┘         └─┘    └┘└─┘ └──┘ └──┘└─┘└─┘ └┘ 
doc  ───────┘                    └┘      └┘          └─┘    └┘ └─┘ └──┘     └─┘    └┘ 
txt  ───────┘                    └┘      └┘          └─┘    └┘ └─┘          └─┘    └┘ 
par  ───────┘                    └┘      └┘          └─┘    └┘ └─┘          └─┘    └┘ 
pid  ───────┘                    └┘      └┘          └─┘    └┘ └─┘          └─┘    └┘ 
st   ─────────────────────────────────────────────────────────────────────────────────────────
247          Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ Hausdorff_dist (p.val) (q.val),
id                                  └─────────────┘        └───┘  └─────────────┘      └────────────┘   └──┘
src  ───────┘                     └─────────────┘  └─┘ └───┘ └─────────────┘  └─┘└────────────┘  └──┘└┘      
typ  ───────┘                     └─────────────┘  └─┘ └───┘ └─────────────┘└─┘└────────────┘  └──┘└┘      
doc  ───────┘                     └─────────────┘  └─┘ └───┘ └─────────────┘  └─┘ └────────────┘      └┘      
txt  ───────┘                                      └─┘                        └─┘                     └┘      
par  ───────┘                                      └─┘                        └─┘                     └┘      
pid  ───────┘                                      └─┘                        └─┘                     └┘      
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
248    { assume p q hp hq bound,
src      └────────────────────┘
typ      └────────────────────┘
doc      └────────────────────┘
txt      └────────────────────┘
par      └────────────────────┘
pid      └────────────────────┘
st   ───┘└────────────────────┘└─
249      rcases eq_to_GH_space_iff.1 hp with ⟨Φ, ⟨Φisom, Φrange⟩⟩,
id              └────────────────┘   └┘
src      └─────┘└────────────────┘└─┘  └────────────────────────┘
typ      └─────┘└────────────────┘└─┘└┘└────────────────────────┘
doc      └─────┘                  └─┘  └────────────────────────┘
txt      └─────┘                  └─┘  └────────────────────────┘
par      └─────┘                  └─┘  └────────────────────────┘
pid                              └─┘  └────────────────────────┘
st   ───────────────────────────────────────────────────────────┘└─
250      rcases eq_to_GH_space_iff.1 hq with ⟨Ψ, ⟨Ψisom, Ψrange⟩⟩,
id              └────────────────┘   └┘
src      └─────┘└────────────────┘└─┘  └────────────────────────┘
typ      └─────┘└────────────────┘└─┘└┘└────────────────────────┘
doc      └─────┘                  └─┘  └────────────────────────┘
txt      └─────┘                  └─┘  └────────────────────────┘
par      └─────┘                  └─┘  └────────────────────────┘
pid                              └─┘  └────────────────────────┘
st   ───────────────────────────────────────────────────────────┘└─
251      have I : diam (range Φ ∪ range Ψ) ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β),
id                              └───┘                                     └──┘  └──┘   └─┘ 
src      └───────┘           └───┘ └┘ └─┘         └─┘    └┘ └─┘ └─┘ └──┘ └──┘└─┘└─┘ 
typ      └───────┘          └───┘└┘ └─┘         └─┘   └┘ └─┘ └─┘ └──┘ └──┘└─┘└─┘
doc      └───────┘            └───┘ └┘ └─┘          └─┘    └┘ └─┘ └─┘ └──┘     └─┘    
txt      └───────┘                  └┘ └─┘          └─┘    └┘ └─┘ └─┘          └─┘    
par      └───────┘                  └┘ └─┘          └─┘    └┘ └─┘ └─┘          └─┘    
pid      └────┘└─┘                  └┘ └─┘          └─┘    └┘ └─┘ └─┘          └─┘    
st   ────────────────────────────────────────────────────────────────────────────────────────────┘└─
252      { rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id                └────────────────────┘ 
src        └─────┘└────────────────────┘ └───────────┘
typ        └─────┘└────────────────────┘└───────────┘
doc        └─────┘                       └───────────┘
txt        └─────┘                       └───────────┘
par        └─────┘                       └───────────┘
pid                                     └───────────┘
st   ─────┘└──────────────────────────────────────────┘└─
253        have : ∃y ∈ range Ψ, dist (Φ xα) y < diam (univ : set α) + 1 + diam (univ : set β),
id                    └───┘  └──┘   └┘                               └──┘  └──┘   └─┘ 
src        └─────┘└──┘└───┘ └──┘    └┘           └─┘    └┘ └─┘ └──┘ └──┘└─┘└─┘ 
typ        └─────┘└──┘└───┘└──┘ └┘└┘           └─┘   └┘ └─┘ └──┘ └──┘└─┘└─┘
doc        └─────┘ └──┘└───┘          └┘           └─┘    └┘ └─┘ └──┘     └─┘    
txt        └─────┘ └──┘               └┘           └─┘    └┘ └─┘          └─┘    
par        └─────┘ └──┘               └┘           └─┘    └┘ └─┘          └─┘    
pid        └───┘└┘ └──┘               └┘           └─┘    └┘ └─┘          └─┘    
st   ───────────────────────────────────────────────────────────────────────────────────────┘└─
254        { rw Ψrange,
id              └────┘
src          └─┘
typ          └─┘└────┘
doc          └─┘
txt          └─┘
par          └─┘
pid            
st   ───────┘└───────┘└─
255          have : Φ xα ∈ p.val := begin rw ← Φrange, exact mem_range_self _ end,
id                   └┘   └───┘               └────┘        └────────────┘
src          └─────┘    └───┘└──┘     └───┘      └┘└────┘└────────────┘└─┘└─┘
typ          └─────┘└┘ └───┘└──┘     └───┘└────┘└┘└────┘└────────────┘└─┘└─┘
doc          └─────┘         └──┘     └───┘      └┘└────┘              └─┘└─┘
txt          └─────┘         └──┘     └───┘      └┘└────┘              └─┘└─┘
par          └─────┘         └──┘     └───┘      └┘└────┘              └─┘└─┘
pid          └───┘└┘         └──┘     └────┘      └──────┘              └────┘
st   ──────────────────────────────┘└───────────────┘└───────────────────────┘└─┘└─
256          exact exists_dist_lt_of_Hausdorff_dist_lt this bound
id                 └─────────────────────────────────┘ └──┘ └───┘
src          └────┘└─────────────────────────────────┘         
typ          └────┘└─────────────────────────────────┘└──┘└───┘
doc          └────┘└─────────────────────────────────┘         
txt          └────┘                                            
par          └────┘                                            
pid                                                           
st   ─────────────────────────────────────────────────────────────
257            (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.2.1 q.2.1 p.2.2.bounded q.2.2.bounded) },
id              └───────────────────────────────────────────┘                          
src  ─────────┘ └───────────────────────────────────────────┘ └───┘ └───┘ └───────────┘ └────────────┘
typ  ─────────┘ └───────────────────────────────────────────┘ └───┘ └───┘└───────────┘└────────────┘
doc  ─────────┘ └───────────────────────────────────────────┘ └───┘ └───┘ └───────────┘ └────────────┘
txt  ─────────┘                                               └───┘ └───┘ └───────────┘ └────────────┘
par  ─────────┘                                               └───┘ └───┘ └───────────┘ └────────────┘
pid  ─────────┘                                               └───┘ └───┘ └───────────┘ └───────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────┘└┘
258        rcases this with ⟨y, hy, dy⟩,
id                └──┘
src        └─────┘    └───────────────┘
typ        └─────┘└──┘└───────────────┘
doc        └─────┘    └───────────────┘
txt        └─────┘    └───────────────┘
par        └─────┘    └───────────────┘
pid                  └───────────────┘
st   ─────────────────────────────────┘└─
259        rcases mem_range.1 hy with ⟨z, hzy⟩,
id                └───────┘   └┘
src        └─────┘└───────┘└─┘  └────────────┘
typ        └─────┘└───────┘└─┘└┘└────────────┘
doc        └─────┘         └─┘  └────────────┘
txt        └─────┘         └─┘  └────────────┘
par        └─────┘         └─┘  └────────────┘
pid                       └─┘  └────────────┘
st   ────────────────────────────────────────┘└─
260        rw ← hzy at dy,
id              └─┘
src        └───┘   └────┘
typ        └───┘└─┘└────┘
doc        └───┘   └────┘
txt        └───┘   └────┘
par        └───┘   └────┘
pid          └─┘   └────┘
st   ───────────────────┘└─
261        have DΦ : diam (range Φ) = diam (univ : set α) :=
id                         └───┘     └──┘  └──┘   └─┘ 
src        └────────┘     └───┘ └┘ └──┘ └──┘└─┘└─┘ └────
typ        └────────┘     └───┘└┘ └──┘ └──┘└─┘└─┘└────
doc        └────────┘     └───┘ └┘ └──┘     └─┘    └────
txt        └────────┘           └┘          └─┘    └────
par        └────────┘           └┘          └─┘    └────
pid        └─────┘└─┘           └┘          └─┘    └───
st   ────────────────────────────────────────────────────────
262          begin rw [← image_univ], apply metric.isometry.diam_image Φisom end,
id                       └────────┘         └────────────────────────┘ └───┘
src  ───────┘     └────┘└────────┘└┘└────┘└────────────────────────┘     └─┘
typ  ───────┘     └────┘└────────┘└┘└────┘└────────────────────────┘└───┘└─┘
doc  ───────┘     └────┘          └┘└────┘└────────────────────────┘     └─┘
txt  ───────┘     └────┘          └┘└────┘                               └─┘
par  ───────┘     └────┘          └┘└────┘                               └─┘
pid  ───────┘     └─────┘          └───────┘                               └──┘
st   ───────┘└────────────────────┘└────────────────────────────────────────┘└─┘└─
263        have DΨ : diam (range Ψ) = diam (univ : set β) :=
id                         └───┘     └──┘  └──┘   └─┘ 
src        └────────┘     └───┘ └┘ └──┘ └──┘└─┘└─┘ └────
typ        └────────┘     └───┘└┘ └──┘ └──┘└─┘└─┘└────
doc        └────────┘     └───┘ └┘ └──┘     └─┘    └────
txt        └────────┘           └┘          └─┘    └────
par        └────────┘           └┘          └─┘    └────
pid        └─────┘└─┘           └┘          └─┘    └───
st   ────────────────────────────────────────────────────────
264          begin rw [← image_univ], apply metric.isometry.diam_image Ψisom end,
id                       └────────┘         └────────────────────────┘ └───┘
src  ───────┘     └────┘└────────┘└┘└────┘└────────────────────────┘     └─┘
typ  ───────┘     └────┘└────────┘└┘└────┘└────────────────────────┘└───┘└─┘
doc  ───────┘     └────┘          └┘└────┘└────────────────────────┘     └─┘
txt  ───────┘     └────┘          └┘└────┘                               └─┘
par  ───────┘     └────┘          └┘└────┘                               └─┘
pid  ───────┘     └─────┘          └───────┘                               └──┘
st   ───────┘└────────────────────┘└────────────────────────────────────────┘└─┘└─
265        calc
id         └──┘
src        └──┘
typ        └──┘
doc        └──┘
st   ───────────
266          diam (range Φ ∪ range Ψ) ≤ diam (range Φ) + dist (Φ xα) (Ψ z) + diam (range Ψ) :
id                                                       └──┘   └┘         └──┘  └───┘ 
src                                                      └──┘                └──┘  └───┘
typ                                                      └──┘   └┘         └──┘  └───┘ 
doc                                                                          └──┘  └───┘
st   ─────────────────────────────────────────────────────────────────────────────────────────
267            diam_union (mem_range_self _) (mem_range_self _)
id             └────────┘                     └────────────┘
src            └────────┘                     └────────────┘
typ            └────────┘                     └────────────┘
doc            └────────┘
st   ───────────────────────────────────────────────────────────
268          ... ≤ diam (univ : set α) + (diam (univ : set α) + 1 + diam (univ : set β)) + diam (univ : set β) :
st   ────────────────────────────────────────────────────────────────────────────────────────────────────────────
269            by { rw [DΦ, DΨ], apply add_le_add (add_le_add (le_refl _) (le_of_lt dy)) (le_refl _) }
id                      └┘  └┘                     └────────┘              └──────┘ └┘    └─────┘
src                 └──┘  └┘    └────┘           └────────┘        └──┘ └──────┘  └─┘ └─────┘└──┘
typ                 └──┘└┘└┘└┘  └────┘           └────────┘        └──┘ └──────┘└┘└─┘ └─────┘└──┘
doc                 └──┘  └┘    └────┘                             └──┘           └─┘        └──┘
txt                 └──┘  └┘    └────┘                             └──┘           └─┘        └──┘
par                 └──┘  └┘    └────┘                             └──┘           └─┘        └──┘
pid                   └┘  └┘                                      └──┘           └─┘        └─┘
st   ───────────┘└───────┘└──┘└─────────────────────────────────────────────────────────────────────┘└┘
270          ... = 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) : by ring },
id                                                        └──┘   └─┘ 
src                                                        └──┘   └─┘         └───┘
typ                                                       └──┘   └─┘        └───┘
doc                                                                           └───┘
txt                                                                           └───┘
par                                                                           └───┘
pid                                                                               
st   └──────────────────────────────────────────────────────────────────────┘└────┘└┘
271  
st   
272      let f : α ⊕ β → ℓ_infty_ℝ := λx, match x with | inl y := Φ y | inr z := Ψ z end,
id                    └───────┘                                            
src      └──────┘   └───────┘└──┘ └─┘      └──────┘    └──┘  └─┘    └──┘  └──┘
typ      └──────┘ └───────┘└──┘ └─┘      └──────┘   └──┘ └─┘   └──┘ └──┘
doc      └──────┘    └───────┘└──┘ └─┘      └──────┘    └──┘  └─┘    └──┘  └──┘
txt      └──────┘             └──┘ └─┘      └──────┘    └──┘  └─┘    └──┘  └──┘
par      └──────┘             └──┘ └─┘      └──────┘    └──┘  └─┘    └──┘  └──┘
pid      └───┘└─┘             └──┘ └─┘      └──────┘    └──┘  └─┘    └──┘  └──┘
st   ──────────────────────────────────────────────────────────────────────────────────┘└─
273      let F : (α ⊕ β) × (α ⊕ β) → ℝ := λp, dist (f p.1) (f p.2),
id                                         └──┘          
src      └──────┘    └┘    └┘  └──┘ └─┘└──┘   └──┘   └─┘
typ      └──────┘    └┘  └┘  └──┘ └─┘└──┘   └──┘  └─┘
doc      └──────┘    └┘     └┘  └──┘ └─┘       └──┘   └─┘
txt      └──────┘    └┘     └┘  └──┘ └─┘       └──┘   └─┘
par      └──────┘    └┘     └┘  └──┘ └─┘       └──┘   └─┘
pid      └───┘└─┘    └┘     └┘  └──┘ └─┘       └──┘   └─┘
st   ────────────────────────────────────────────────────────────┘└─
274      -- check that the induced "distance" is a candidate
st   ────────────────────────────────────────────────────────
275      have Fgood : F ∈ candidates α β,
id                       └────────┘  
src      └───────────┘  └────────┘ 
typ      └───────────┘ └────────┘
doc      └───────────┘  └────────┘ 
txt      └───────────┘             
par      └───────────┘             
pid      └────────┘└─┘             
st   ──────────────────────────────────┘└─
276      { simp only [candidates, forall_const, and_true, add_comm, eq_self_iff_true, dist_eq_zero,
id                    └────────┘  └──────────┘  └──────┘  └──────┘  └──────────────┘  └──────────┘
src        └─────────┘└────────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└──────────┘└─
typ        └─────────┘└────────┘└┘└──────────┘└┘└──────┘└┘└──────┘└┘└──────────────┘└┘└──────────┘└─
doc        └─────────┘└────────┘└┘            └┘        └┘        └┘                └┘            └─
txt        └─────────┘          └┘            └┘        └┘        └┘                └┘            └─
par        └─────────┘          └┘            └┘        └┘        └┘                └┘            └─
pid            └──┘└┘          └┘            └┘        └┘        └┘                └┘            └─
st   ─────┘└────────────────────────────────────────────────────────────────────────────────────────
277                   and_self, set.mem_set_of_eq],
id                    └──────┘  └───────────────┘
src  ────────────────┘└──────┘└┘└───────────────┘
typ  ────────────────┘└──────┘└┘└───────────────┘
doc  ────────────────┘        └┘                 
txt  ────────────────┘        └┘                 
par  ────────────────┘        └┘                 
pid  ────────────────┘        └┘                 
st   ────────────────────────────────────────────┘└─
278        repeat {split},
src        └──────┘└───┘
typ        └──────┘└───┘
doc        └──────┘└───┘
txt        └──────┘└───┘
par        └──────┘└───┘
pid              └──────┘
st   ──────────────────┘└┘
279        { exact λx y, calc
src          └────┘ └───┘    
typ          └────┘ └───┘    
doc          └────┘ └───┘    
txt          └────┘ └───┘    
par          └────┘ └───┘    
pid                └───┘    
st   ───────┘└────────────────
280          F (inl x, inl y) = dist (Φ x) (Φ y) : rfl
id                    └─┘                        └─┘
src  ───────┘      └┘└─┘ └┘        └┘   └──┘└─┘
typ  ───────┘     └┘└─┘ └┘        └┘  └──┘└─┘
doc  ───────┘      └┘    └┘        └┘   └──┘   
txt  ───────┘      └┘    └┘        └┘   └──┘   
par  ───────┘      └┘    └┘        └┘   └──┘   
pid  ───────┘      └┘    └┘        └┘   └──┘   
st   ──────────────────────────────────────────────────
281          ... = dist x y : Φisom.dist_eq },
id                 └──┘       └───────────┘
src  ───────────┘ └──┘  └─┘└───────────┘
typ  ───────────┘ └──┘  └─┘└───────────┘
doc  ───────────┘       └─┘└───────────┘
txt  ───────────┘       └─┘             
par  ───────────┘       └─┘             
pid  ───────────┘       └─┘             
st   ──────────────────────────────────────┘└┘
282        { exact λx y, calc
src          └────┘ └───┘    
typ          └────┘ └───┘    
doc          └────┘ └───┘    
txt          └────┘ └───┘    
par          └────┘ └───┘    
pid                └───┘    
st   ───────┘└────────────────
283          F (inr x, inr y) = dist (Ψ x) (Ψ y) : rfl
id                    └─┘                        └─┘
src  ───────┘      └┘└─┘ └┘        └┘   └──┘└─┘
typ  ───────┘     └┘└─┘ └┘        └┘  └──┘└─┘
doc  ───────┘      └┘    └┘        └┘   └──┘   
txt  ───────┘      └┘    └┘        └┘   └──┘   
par  ───────┘      └┘    └┘        └┘   └──┘   
pid  ───────┘      └┘    └┘        └┘   └──┘   
st   ──────────────────────────────────────────────────
284          ... = dist x y : Ψisom.dist_eq },
id                 └──┘       └───────────┘
src  ───────────┘ └──┘  └─┘└───────────┘
typ  ───────────┘ └──┘  └─┘└───────────┘
doc  ───────────┘       └─┘└───────────┘
txt  ───────────┘       └─┘             
par  ───────────┘       └─┘             
pid  ───────────┘       └─┘             
st   ──────────────────────────────────────┘└┘
285        { exact λx y, dist_comm _ _ },
id                       └───────┘
src          └────┘ └───┘└───────┘└───┘
typ          └────┘ └───┘└───────┘└───┘
doc          └────┘ └───┘         └───┘
txt          └────┘ └───┘         └───┘
par          └────┘ └───┘         └───┘
pid                └───┘         └──┘
st   ───────┘└────────────────────────┘└┘
286        { exact λx y z, dist_triangle _ _ _ },
id                         └───────────┘
src          └────┘ └─────┘└───────────┘└─────┘
typ          └────┘ └─────┘└───────────┘└─────┘
doc          └────┘ └─────┘             └─────┘
txt          └────┘ └─────┘             └─────┘
par          └────┘ └─────┘             └─────┘
pid                └─────┘             └────┘
st   ───────┘└────────────────────────────────┘└┘
287        { exact λx y, calc
src          └────┘ └───┘    
typ          └────┘ └───┘    
doc          └────┘ └───┘    
txt          └────┘ └───┘    
par          └────┘ └───┘    
pid                └───┘    
st   ─────────────────────────
288          F (x, y) ≤ diam (range Φ ∪ range Ψ) :
id                                    └───┘ 
src  ───────┘   └┘ └┘             └───┘ └───
typ  ───────┘  └┘ └┘            └───┘└───
doc  ───────┘   └┘ └┘             └───┘ └───
txt  ───────┘   └┘ └┘                   └───
par  ───────┘   └┘ └┘                   └───
pid  ───────┘   └┘ └┘                   └───
st   ──────────────────────────────────────────────
289          begin
src  ───────┘     
typ  ───────┘     
doc  ───────┘     
txt  ───────┘     
par  ───────┘     
pid  ───────┘     
st   ───────┘└─────
290            have A : ∀z : α ⊕ β, f z ∈ range Φ ∪ range Ψ,
id                                              └───┘ 
src  ─────────┘└───────┘ └──┘              └───┘ └─
typ  ─────────┘└───────┘ └──┘          └───┘└─
doc  ─────────┘└───────┘ └──┘              └───┘ └─
txt  ─────────┘└───────┘ └──┘                    └─
par  ─────────┘└───────┘ └──┘                    └─
pid  ──────────────────┘ └──┘                    └─
st   ─────────────────────────────────────────────────────┘└─
291            { assume z,
src  ───────────┘└──────┘└─
typ  ───────────┘└──────┘└─
doc  ───────────┘└──────┘└─
txt  ───────────┘└──────┘└─
par  ───────────┘└──────┘└─
pid  ──────────────────────
st   ──────────┘└───────┘└─
292              cases z,
id                     
src  ───────────┘└────┘ └─
typ  ───────────┘└────┘└─
doc  ───────────┘└────┘ └─
txt  ───────────┘└────┘ └─
par  ───────────┘└────┘ └─
pid  ─────────────────┘ └─
st   ──────────────────┘└─
293              { apply mem_union_left, apply mem_range_self },
id                       └────────────┘        └────────────┘
src  ─────────────┘└────┘└────────────┘└┘└────┘└────────────┘└──
typ  ───────────────────┘└────────────┘└──────┘└────────────┘└───
doc  ─────────────┘└────┘              └┘└────┘              └──
txt  ─────────────┘└────┘              └┘└────┘              └──
par  ───────────────────┘              └──────┘              └───
pid  ───────────────────┘              └──────┘              └───
st   ────────────┘└───────────────────┘└─────────────────────┘└─
294              { apply mem_union_right, apply mem_range_self } },
id                       └─────────────┘        └────────────┘
src  ─────────────┘└────┘└─────────────┘└┘└────┘└────────────┘└────
typ  ───────────────────┘└─────────────┘└──────┘└────────────┘└─────
doc  ─────────────┘└────┘               └┘└────┘              └────
txt  ─────────────┘└────┘               └┘└────┘              └────
par  ───────────────────┘               └──────┘              └─────
pid  ───────────────────┘               └──────┘              └─────
st   ──────────────────────────────────┘└─────────────────────┘└─┘└─
295            refine dist_le_diam_of_mem _ (A _) (A _),
id                    └─────────────────┘          
src  ─────────┘└─────┘└─────────────────┘└─┘  └──┘  └─┘└─
typ  ────────────────┘└─────────────────┘└─┘  └──┘ └────
doc  ─────────┘└─────┘└─────────────────┘└─┘  └──┘  └─┘└─
txt  ─────────┘└─────┘                   └─┘  └──┘  └─┘└─
par  ────────────────┘                   └─┘  └──┘  └────
pid  ────────────────┘                   └─┘  └──┘  └────
st   ─────────────────────────────────────────────────┘└─
296            rw [Φrange, Ψrange],
id                 └────┘  └────┘
src  ─────────┘└──┘      └┘      └─
typ  ─────────┘└──┘└────┘└┘└────┘└─
doc  ─────────┘└──┘      └┘      └─
txt  ─────────┘└──┘      └┘      └─
par  ─────────┘└──┘      └┘      └─
pid  ─────────────┘      └┘      └──
st   ───────────────────┘└──────┘└──
297            exact (p.2.2.union q.2.2).bounded,
id                               
src  ───────────────┘  └─────────┘ └──────────────
typ  ───────────────┘ └─────────┘└──────────────
doc  ───────────────┘  └─────────┘ └──────────────
txt  ───────────────┘  └─────────┘ └──────────────
par  ───────────────┘  └─────────┘ └──────────────
pid  ───────────────┘  └─────────┘ └──────────────
st   ──────────────────────────────────────────┘└─
298          end
src  ────────────
typ  ────────────
doc  ────────────
txt  ────────────
par  ────────────
pid  ────────────
st   ──────────┘
299          ... ≤ 2 * diam (univ : set α) + 1 + 2 * diam (univ : set β) : I } },
id                                                  └──┘  └──┘   └─┘     
src  ───────────┘ └─┘          └─┘    └┘ └─┘ └─┘ └──┘ └──┘└─┘└─┘ └──┘ 
typ  ───────────┘ └─┘          └─┘   └┘ └─┘ └─┘ └──┘ └──┘└─┘└─┘└──┘
doc  ───────────┘ └─┘          └─┘    └┘ └─┘ └─┘ └──┘     └─┘    └──┘ 
txt  ───────────┘ └─┘          └─┘    └┘ └─┘ └─┘          └─┘    └──┘ 
par  ───────────┘ └─┘          └─┘    └┘ └─┘ └─┘          └─┘    └──┘ 
pid  ───────────┘ └─┘          └─┘    └┘ └─┘ └─┘          └─┘    └──┘ 
st   ───────────────────────────────────────────────────────────────────────┘└──┘
300      let Fb := candidates_b_of_candidates F Fgood,
id                 └────────────────────────┘  └───┘
src      └────────┘└────────────────────────┘ 
typ      └────────┘└────────────────────────┘└───┘
doc      └────────┘└────────────────────────┘ 
txt      └────────┘                           
par      └────────┘                           
pid      └────┘└─┘                           
st   ───────────────────────────────────────────────┘└─
301      have : Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ HD Fb :=
id              └────────────┘         └─────────────┘        └───┘  └─────────────┘       └┘ └┘
src      └─────┘└────────────┘       └─────────────┘  └─┘ └───┘ └─────────────┘  └─┘ └┘  └───
typ      └─────┘└────────────┘       └─────────────┘  └─┘ └───┘ └─────────────┘└─┘ └┘└┘└───
doc      └─────┘└────────────┘       └─────────────┘  └─┘ └───┘ └─────────────┘  └─┘ └┘  └───
txt      └─────┘                                      └─┘                        └─┘     └───
par      └─────┘                                      └─┘                        └─┘     └───
pid      └───┘└┘                                      └─┘                        └─┘     └───
st   ─────────────────────────────────────────────────────────────────────────────────────────────────
302        Hausdorff_dist_optimal_le_HD _ _ (candidates_b_of_candidates_mem F Fgood),
id         └──────────────────────────┘      └────────────────────────────┘  └───┘
src  ─────┘└──────────────────────────┘└───┘ └────────────────────────────┘      
typ  ─────┘└──────────────────────────┘└───┘ └────────────────────────────┘└───┘
doc  ─────┘└──────────────────────────┘└───┘                                     
txt  ─────┘                            └───┘                                     
par  ─────┘                            └───┘                                     
pid  ─────┘                            └───┘                                     
st   ──────────────────────────────────────────────────────────────────────────────┘└─
303      refine le_trans this (le_of_forall_le_of_dense (λr hr, _)),
id              └──────┘ └──┘  └──────────────────────┘
src      └─────┘└──────┘     └──────────────────────┘  └───────┘
typ      └─────┘└──────┘└──┘ └──────────────────────┘  └───────┘
doc      └─────┘                                       └───────┘
txt      └─────┘                                       └───────┘
par      └─────┘                                       └───────┘
pid                                                   └───────┘
st   ─────────────────────────────────────────────────────────────┘└─
304      have I1 : ∀x : α, infi (λy:β, Fb (inl x, inr y)) ≤ r,
id                        └──┘       └┘ └─┘    └─┘       
src      └────────┘ └──┘  └──┘  └┘ └┘  └─┘ └┘└─┘ └─┘ 
typ      └────────┘ └──┘ └──┘  └┘└┘└┘└─┘ └┘└─┘ └─┘ 
doc      └────────┘ └──┘  └──┘  └┘ └┘       └┘    └─┘ 
txt      └────────┘ └──┘        └┘ └┘       └┘    └─┘ 
par      └────────┘ └──┘        └┘ └┘       └┘    └─┘ 
pid      └─────┘└─┘ └──┘        └┘ └┘       └┘    └─┘ 
st   ───────────────────────────────────────────────────────┘└─
305      { assume x,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
306        have : f (inl x) ∈ p.val, by { rw [← Φrange], apply mem_range_self },
id                  └─┘     └───┘             └────┘         └────────────┘
src        └─────┘  └─┘ └┘ └───┘       └────┘        └────┘└────────────┘
typ        └─────┘ └─┘└┘ └───┘       └────┘└────┘  └────┘└────────────┘
doc        └─────┘      └┘             └────┘        └────┘              
txt        └─────┘      └┘             └────┘        └────┘              
par        └─────┘      └┘             └────┘        └────┘              
pid        └───┘└┘      └┘               └──┘                           
st   ─────────────────────────────┘     └───────────┘└──────────────────────┘└┘
307        rcases exists_dist_lt_of_Hausdorff_dist_lt this hr
id                └─────────────────────────────────┘ └──┘ └┘
src        └─────┘└─────────────────────────────────┘      
typ        └─────┘└─────────────────────────────────┘└──┘└┘
doc        └─────┘└─────────────────────────────────┘      
txt        └─────┘                                         
par        └─────┘                                         
pid                                                       
st   ─────────────────────────────────────────────────────────
308          (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.2.1 q.2.1 p.2.2.bounded q.2.2.bounded)
id            └───────────────────────────────────────────┘                          
src  ───────┘ └───────────────────────────────────────────┘ └───┘ └───┘ └───────────┘ └─────────────
typ  ───────┘ └───────────────────────────────────────────┘ └───┘ └───┘└───────────┘└─────────────
doc  ───────┘ └───────────────────────────────────────────┘ └───┘ └───┘ └───────────┘ └─────────────
txt  ───────┘                                               └───┘ └───┘ └───────────┘ └─────────────
par  ───────┘                                               └───┘ └───┘ └───────────┘ └─────────────
pid  ───────┘                                               └───┘ └───┘ └───────────┘ └─────────────
st   ────────────────────────────────────────────────────────────────────────────────────────────────
309          with ⟨z, zq, hz⟩,
src  ───────────────────────┘
typ  ───────────────────────┘
doc  ───────────────────────┘
txt  ───────────────────────┘
par  ───────────────────────┘
pid  ───────────────────────┘
st   ───────────────────────┘└─
310        have : z ∈ range Ψ, by rwa [← Ψrange] at zq,
id                   └───┘             └────┘
src        └─────┘  └───┘      └─────┘      └─────┘
typ        └─────┘ └───┘     └─────┘└────┘└─────┘
doc        └─────┘  └───┘      └─────┘      └─────┘
txt        └─────┘             └─────┘      └─────┘
par        └─────┘             └─────┘      └─────┘
pid        └───┘└┘                └──┘      └────┘
st   ───────────────────────┘          └──────┘      └─
311        rcases mem_range.1 this with ⟨y, hy⟩,
id                └───────┘   └──┘
src        └─────┘└───────┘└─┘    └───────────┘
typ        └─────┘└───────┘└─┘└──┘└───────────┘
doc        └─────┘         └─┘    └───────────┘
txt        └─────┘         └─┘    └───────────┘
par        └─────┘         └─┘    └───────────┘
pid                       └─┘    └───────────┘
st   ─────────────────────────────────────────┘└─
312        calc infi (λy:β, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :
id         └──┘ └──┘                            └┘  └─┘   └─┘ 
src        └──┘ └──┘                                 └─┘    └─┘
typ        └──┘ └──┘                            └┘  └─┘   └─┘ 
doc        └──┘ └──┘
st   ────────────────────────────────────────────────────────────────
313            cinfi_le (by simpa using HD_below_aux1 0)
id             └──────┘                 └───────────┘
src            └──────┘     └──────────┘└───────────┘└┘
typ            └──────┘     └──────────┘└───────────┘└┘
doc            └──────┘     └──────────┘             └┘
txt                         └──────────┘             └┘
par                         └──────────┘             └┘
pid                              └────┘             
st   ─────────────────────┘└──────────────────────────┘└─
314          ... = dist (Φ x) (Ψ y) : rfl
id                 └──┘             └─┘
src                └──┘               └─┘
typ                └──┘             └─┘
st   ─────────────────────────────────────
315          ... = dist (f (inl x)) z : by rw hy
id                                          └┘
src                                        └─┘  
typ                                      └─┘└┘
doc                                        └─┘  
txt                                        └─┘  
par                                        └─┘  
pid                                            
st   ────────────────────────────────────┘└──────
316          ... ≤ r : le_of_lt hz },
id                    └──────┘ └┘
src  ───────┘          └──────┘
typ  ───────┘         └──────┘ └┘
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘└───────────────────┘└─┘
317      have I2 : ∀y : β, infi (λx:α, Fb (inl x, inr y)) ≤ r,
id                        └──┘       └┘ └─┘    └─┘       
src      └────────┘ └──┘  └──┘  └┘ └┘  └─┘ └┘└─┘ └─┘ 
typ      └────────┘ └──┘ └──┘  └┘└┘└┘└─┘ └┘└─┘ └─┘ 
doc      └────────┘ └──┘  └──┘  └┘ └┘       └┘    └─┘ 
txt      └────────┘ └──┘        └┘ └┘       └┘    └─┘ 
par      └────────┘ └──┘        └┘ └┘       └┘    └─┘ 
pid      └─────┘└─┘ └──┘        └┘ └┘       └┘    └─┘ 
st   ───────────────────────────────────────────────────────┘└─
318      { assume y,
src        └──────┘
typ        └──────┘
doc        └──────┘
txt        └──────┘
par        └──────┘
pid        └──────┘
st   ─────┘└──────┘└─
319        have : f (inr y) ∈ q.val, by { rw [← Ψrange], apply mem_range_self },
id                  └─┘     └───┘             └────┘         └────────────┘
src        └─────┘  └─┘ └┘ └───┘       └────┘        └────┘└────────────┘
typ        └─────┘ └─┘└┘ └───┘       └────┘└────┘  └────┘└────────────┘
doc        └─────┘      └┘             └────┘        └────┘              
txt        └─────┘      └┘             └────┘        └────┘              
par        └─────┘      └┘             └────┘        └────┘              
pid        └───┘└┘      └┘               └──┘                           
st   ─────────────────────────────┘     └───────────┘└──────────────────────┘└┘
320        rcases exists_dist_lt_of_Hausdorff_dist_lt' this hr
id                └──────────────────────────────────┘ └──┘ └┘
src        └─────┘└──────────────────────────────────┘      
typ        └─────┘└──────────────────────────────────┘└──┘└┘
doc        └─────┘└──────────────────────────────────┘      
txt        └─────┘                                          
par        └─────┘                                          
pid                                                        
st   ──────────────────────────────────────────────────────────
321          (Hausdorff_edist_ne_top_of_nonempty_of_bounded p.2.1 q.2.1 p.2.2.bounded q.2.2.bounded)
id            └───────────────────────────────────────────┘                          
src  ───────┘ └───────────────────────────────────────────┘ └───┘ └───┘ └───────────┘ └─────────────
typ  ───────┘ └───────────────────────────────────────────┘ └───┘ └───┘└───────────┘└─────────────
doc  ───────┘ └───────────────────────────────────────────┘ └───┘ └───┘ └───────────┘ └─────────────
txt  ───────┘                                               └───┘ └───┘ └───────────┘ └─────────────
par  ───────┘                                               └───┘ └───┘ └───────────┘ └─────────────
pid  ───────┘                                               └───┘ └───┘ └───────────┘ └─────────────
st   ────────────────────────────────────────────────────────────────────────────────────────────────
322          with ⟨z, zq, hz⟩,
src  ───────────────────────┘
typ  ───────────────────────┘
doc  ───────────────────────┘
txt  ───────────────────────┘
par  ───────────────────────┘
pid  ───────────────────────┘
st   ───────────────────────┘└─
323        have : z ∈ range Φ, by rwa [← Φrange] at zq,
id                   └───┘             └────┘
src        └─────┘  └───┘      └─────┘      └─────┘
typ        └─────┘ └───┘     └─────┘└────┘└─────┘
doc        └─────┘  └───┘      └─────┘      └─────┘
txt        └─────┘             └─────┘      └─────┘
par        └─────┘             └─────┘      └─────┘
pid        └───┘└┘                └──┘      └────┘
st   ───────────────────────┘          └──────┘      └─
324        rcases mem_range.1 this with ⟨x, hx⟩,
id                └───────┘   └──┘
src        └─────┘└───────┘└─┘    └───────────┘
typ        └─────┘└───────┘└─┘└──┘└───────────┘
doc        └─────┘         └─┘    └───────────┘
txt        └─────┘         └─┘    └───────────┘
par        └─────┘         └─┘    └───────────┘
pid                       └─┘    └───────────┘
st   ─────────────────────────────────────────┘└─
325        calc infi (λx:α, Fb (inl x, inr y)) ≤ Fb (inl x, inr y) :
id         └──┘ └──┘                            └┘  └─┘   └─┘ 
src        └──┘ └──┘                                 └─┘    └─┘
typ        └──┘ └──┘                            └┘  └─┘   └─┘ 
doc        └──┘ └──┘
st   ────────────────────────────────────────────────────────────────
326            cinfi_le (by simpa using HD_below_aux2 0)
id             └──────┘                 └───────────┘
src            └──────┘     └──────────┘└───────────┘└┘
typ            └──────┘     └──────────┘└───────────┘└┘
doc            └──────┘     └──────────┘             └┘
txt                         └──────────┘             └┘
par                         └──────────┘             └┘
pid                              └────┘             
st   ─────────────────────┘└──────────────────────────┘└─
327          ... = dist (Φ x) (Ψ y) : rfl
id                 └──┘             └─┘
src                └──┘               └─┘
typ                └──┘             └─┘
st   ─────────────────────────────────────
328          ... = dist z (f (inr y)) : by rw hx
id                                          └┘
src                                        └─┘  
typ                                      └─┘└┘
doc                                        └─┘  
txt                                        └─┘  
par                                        └─┘  
pid                                            
st   ────────────────────────────────────┘└──────
329          ... ≤ r : le_of_lt hz },
id                    └──────┘ └┘
src  ───────┘          └──────┘
typ  ───────┘         └──────┘ └┘
doc  ───────┘
txt  ───────┘
par  ───────┘
pid  ───────┘
st   ───────┘└───────────────────┘└─┘
330      simp [HD, csupr_le I1, csupr_le I2] },
id             └┘  └──────┘ └┘  └──────┘ └┘
src      └────┘└┘└┘└──────┘  └┘└──────┘  └┘
typ      └────┘└┘└┘└──────┘└┘└┘└──────┘└┘└┘
doc      └────┘└┘└┘└──────┘  └┘└──────┘  └┘
txt      └────┘  └┘          └┘          └┘
par      └────┘  └┘          └┘          └┘
pid            └┘          └┘          
st   ───────────────────────────────────────┘└┘
331    /- Get the same inequality for any coupling. If the coupling is quite good, the desired
st   ──────────────────────────────────────────────────────────────────────────────────────────
332    inequality has been proved above. If it is bad, then the inequality is obvious. -/
st   ─────────────────────────────────────────────────────────────────────────────────────
333    have B : ∀p q : nonempty_compacts (ℓ_infty_ℝ), ⟦p⟧ = to_GH_space α → ⟦q⟧ = to_GH_space β →
id                     └───────────────┘  └───────┘                               └─────────┘
src    └───────┘ └────┘└───────────────┘ └───────┘                      └─────────┘  
typ    └───────┘ └────┘└───────────────┘ └───────┘                      └─────────┘  
doc    └───────┘ └────┘└───────────────┘ └───────┘                      └─────────┘  
txt    └───────┘ └────┘                                                              
par    └───────┘ └────┘                                                              
pid    └────┘└─┘ └────┘                                                              
st   ─────────────────────────────────────────────────────────────────────────────────────────────
334          Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ Hausdorff_dist (p.val) (q.val),
id                                  └─────────────┘        └───┘  └─────────────┘       └────────────┘
src  ───────┘                     └─────────────┘  └─┘ └───┘ └─────────────┘  └─┘ └────────────┘      └┘      
typ  ───────┘                     └─────────────┘  └─┘ └───┘ └─────────────┘└─┘ └────────────┘      └┘      
doc  ───────┘                     └─────────────┘  └─┘ └───┘ └─────────────┘  └─┘ └────────────┘      └┘      
txt  ───────┘                                      └─┘                        └─┘                     └┘      
par  ───────┘                                      └─┘                        └─┘                     └┘      
pid  ───────┘                                      └─┘                        └─┘                     └┘      
st   ──────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘└─
335    { assume p q hp hq,
src      └──────────────┘
typ      └──────────────┘
doc      └──────────────┘
txt      └──────────────┘
par      └──────────────┘
pid      └──────────────┘
st   ───┘└──────────────┘└─
336      by_cases h : Hausdorff_dist (p.val) (q.val) < diam (univ : set α) + 1 + diam (univ : set β),
id                    └────────────┘  └───┘   └───┘                             └──┘  └──┘   └─┘ 
src      └───────┘ └─┘└────────────┘ └───┘└┘ └───┘└┘          └─┘    └┘ └─┘ └──┘ └──┘└─┘└─┘ 
typ      └───────┘ └─┘└────────────┘ └───┘└┘ └───┘└┘          └─┘   └┘ └─┘ └──┘ └──┘└─┘└─┘
doc      └───────┘ └─┘└────────────┘      └┘      └┘          └─┘    └┘ └─┘ └──┘     └─┘    
txt      └───────┘ └─┘                    └┘      └┘          └─┘    └┘ └─┘          └─┘    
par      └───────┘ └─┘                    └┘      └┘          └─┘    └┘ └─┘          └─┘    
pid               └─┘                    └┘      └┘          └─┘    └┘ └─┘          └─┘    
st   ──────────────────────────────────────────────────────────────────────────────────────────────┘└─
337      { exact A p q hp hq h },
id                  └┘ └┘ 
src        └────┘        
typ        └────┘└┘└┘
doc        └────┘        
txt        └────┘        
par        └────┘        
pid                     
st   ─────┘└──────────────────┘└┘
338      { calc Hausdorff_dist (range (optimal_GH_injl α β)) (range (optimal_GH_injr α β)) ≤ HD (candidates_b_dist α β) :
id         └──┘                        └─────────────┘        └───┘  └─────────────┘         └┘  └───────────────┘  
src        └──┘                        └─────────────┘        └───┘  └─────────────┘         └┘  └───────────────┘
typ        └──┘                        └─────────────┘        └───┘  └─────────────┘         └┘  └───────────────┘  
doc        └──┘                        └─────────────┘        └───┘  └─────────────┘         └┘
st   ─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────
339               Hausdorff_dist_optimal_le_HD _ _ (candidates_b_dist_mem_candidates_b)
id                └──────────────────────────┘      └────────────────────────────────┘
src               └──────────────────────────┘      └────────────────────────────────┘
typ               └──────────────────────────┘      └────────────────────────────────┘
doc               └──────────────────────────┘
st   ───────────────────────────────────────────────────────────────────────────────────
340             ... ≤ diam (univ : set α) + 1 + diam (univ : set β) : HD_candidates_b_dist_le
id                                              └──┘  └──┘   └─┘      └─────────────────────┘
src                                             └──┘  └──┘   └─┘      └─────────────────────┘
typ                                             └──┘  └──┘   └─┘      └─────────────────────┘
doc                                             └──┘                  └─────────────────────┘
st   ─────────────────────────────────────────────────────────────────────────────────────────
341             ... ≤ Hausdorff_dist (p.val) (q.val) : not_lt.1 h } },
id                    └────────────┘  └───┘   └───┘    └────┘  
src                   └────────────┘  └───┘   └───┘    └────┘
typ                   └────────────┘  └───┘   └───┘    └────┘  
doc                   └────────────┘
st   ───────────────────────────────────────────────────────────┘└───┘
342    refine le_antisymm _ _,
id            └─────────┘
src    └─────┘└─────────┘└──┘
typ    └─────┘└─────────┘└──┘
doc    └─────┘           └──┘
txt    └─────┘           └──┘
par    └─────┘           └──┘
pid                     └──┘
st   ───────────────────────┘└─
343    { apply le_cInf,
id             └─────┘
src      └────┘└─────┘
typ      └────┘└─────┘
doc      └────┘
txt      └────┘
par      └────┘
pid           
st   ───┘└───────────┘
344      { refine (set.nonempty.prod _ _).image _; exact ⟨_, rfl⟩ },
st                                                                └┘
345      { rintro b ⟨⟨p, q⟩, ⟨hp, hq⟩, rfl⟩,
346        exact B p q hp hq } },
st                           └──┘
347    { exact GH_dist_le_Hausdorff_dist (isometry_optimal_GH_injl α β) (isometry_optimal_GH_injr α β) }
id                                                                                                 
typ                                                                                                
st                                                                                                     └─
348  end
st   ──┘
349  
350  /-- The Gromov-Hausdorff distance can also be realized by a coupling in `ℓ^∞(ℝ)`, by embedding
351  the optimal coupling through its Kuratowski embedding. -/
352  theorem GH_dist_eq_Hausdorff_dist (α : Type u) [metric_space α] [compact_space α] [nonempty α]
id                                                     └──┘  └──┘                     └──┘  └┘ 
src                                                    └──┘  └──┘                       └──┘  └┘
typ                                                    └──┘  └──┘                     └──┘  └┘ 
doc                                                    └──┘  └──┘
353    (β : Type v) [metric_space β] [compact_space β] [nonempty β] :
id                     └──┘  └─┘                     └──┘  └┘ 
src                    └──┘  └─┘                       └──┘  └┘
typ                    └──┘  └─┘                     └──┘  └┘ 
doc                    └──┘  └─┘
354    ∃Φ : α → ℓ_infty_ℝ, ∃Ψ : β → ℓ_infty_ℝ, isometry Φ ∧ isometry Ψ ∧
id             └───────┘         └───────┘                       
src             └───────┘           └───────┘                         
typ            └───────┘         └───────┘                       
doc             └───────┘           └───────┘
355    GH_dist α β = Hausdorff_dist (range Φ) (range Ψ) :=
id                                                
typ                                               
356  begin
357    let F := Kuratowski_embedding (optimal_GH_coupling α β),
id                                                         
typ                                                        
358    let Φ := F ∘ optimal_GH_injl α β,
id                                   
typ                                  
359    let Ψ := F ∘ optimal_GH_injr α β,
id                                   
typ                                  
360    refine ⟨Φ, Ψ, _, _, _⟩,
id               
typ              
361    { exact (Kuratowski_embedding.isometry _).comp (isometry_optimal_GH_injl α β) },
id                                                                               
typ                                                                              
st                                                                                   └┘
362    { exact (Kuratowski_embedding.isometry _).comp (isometry_optimal_GH_injr α β) },
id                                                                               
typ                                                                              
st                                                                                   └┘
363    { rw [← image_univ, ← image_univ, image_comp F, image_univ, image_comp F (optimal_GH_injr α β),
id                                                                                                
typ                                                                                               
364        image_univ, ← Hausdorff_dist_optimal],
365      exact (Hausdorff_dist_image (Kuratowski_embedding.isometry _)).symm },
st                                                                           └┘
366  end
st   └─┘
367  
368  -- without the next two lines, `{ exact closed_of_compact (range Φ) hΦ }` in the next
369  -- proof is very slow, as the `t2_space` instance is very hard to find
370  local attribute [instance, priority 10] order_topology.t2_space
id                                           └─────────────────────┘
src                                          └─────────────────────┘
typ                                          └─────────────────────┘
371  local attribute [instance, priority 10] order_closed_topology.to_t2_space
id                                           └───────────────────────────────┘
src                                          └───────────────────────────────┘
typ                                          └───────────────────────────────┘
372  
373  /-- The Gromov-Hausdorff distance defines a genuine distance on the Gromov-Hausdorff space. -/
374  instance GH_space_metric_space : metric_space GH_space :=
id                                    └──────────┘ └──────┘
src                                   └──────────┘ └──────┘
typ                                   └──────────┘ └──────┘
doc                                   └──────────┘ └──────┘
375  { dist_self := λx, begin
id                  
src  
typ                 
st                      └─────
376      rcases exists_rep x with ⟨y, hy⟩,
id              └────────┘ 
src      └─────┘└────────┘ └───────────┘
typ      └─────┘└────────┘└───────────┘
doc      └─────┘           └───────────┘
txt      └─────┘           └───────────┘
par      └─────┘           └───────────┘
pid                       └───────────┘
st   ───────────────────────────────────┘└─
377      refine le_antisymm _ _,
id              └─────────┘
src      └─────┘└─────────┘└──┘
typ      └─────┘└─────────┘└──┘
doc      └─────┘           └──┘
txt      └─────┘           └──┘
par      └─────┘           └──┘
pid                       └──┘
st   ─────────────────────────┘└─
378      { apply cInf_le,
id               └─────┘
src        └────┘└─────┘
typ        └────┘└─────┘
doc        └────┘
txt        └────┘
par        └────┘
pid             
st   ─────┘└───────────┘
379        { exact ⟨0, by { rintro b ⟨⟨u, v⟩, ⟨hu, hv⟩, rfl⟩, exact Hausdorff_dist_nonneg } ⟩},
src          └┘
typ          └┘
doc          └┘
txt          └┘
par          └┘
st           └┘                                                                           └┘ └┘
380        { simp, existsi [y, y], simpa } },
st                                       └──┘
381      { apply le_cInf,
382        { exact (nonempty.prod ⟨y, hy⟩ ⟨y, hy⟩).image _ },
st                                                         └┘
383        { rintro b ⟨⟨u, v⟩, ⟨hu, hv⟩, rfl⟩, exact Hausdorff_dist_nonneg } },
st                                                                         └──┘
384    end,
st     └─┘
385    dist_comm := λx y, begin
id                    
typ                   
386      have A : (λ (p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
387                   Hausdorff_dist ((p.fst).val) ((p.snd).val)) '' (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y})
388             = ((λ (p : nonempty_compacts ℓ_infty_ℝ × nonempty_compacts ℓ_infty_ℝ),
id                                                                         └───────┘
src                                                                        └───────┘
typ                                                                        └───────┘
doc                                                                        └───────┘
389                   Hausdorff_dist ((p.fst).val) ((p.snd).val)) ∘ prod.swap) '' (set.prod {a | ⟦a⟧ = x} {b | ⟦b⟧ = y}) :=
id                                                                                                                  
typ                                                                                                                 
390        by { congr, funext, simp, rw Hausdorff_dist_comm },
st                                                          └┘
391      simp only [dist, A, image_comp, prod.swap, image_swap_prod],
392    end,
st     └─┘
393    eq_of_dist_eq_zero := λx y hxy, begin
id                             
typ                            
394      /- To show that two spaces at zero distance are isometric, we argue that the distance
395      is realized by some coupling. In this coupling, the two spaces are at zero Hausdorff distance,
396      i.e., they coincide. Therefore, the original spaces are isometric. -/
397      rcases GH_dist_eq_Hausdorff_dist x.rep y.rep with ⟨Φ, Ψ, Φisom, Ψisom, DΦΨ⟩,
id                                        └───┘ └───┘
src                                       └───┘ └───┘
typ                                       └───┘ └───┘
doc                                       └───┘ └───┘
398      rw [← dist_GH_dist, hxy] at DΦΨ,
399      have : range Φ = range Ψ,
id                             
typ                            
400      { have hΦ : compact (range Φ) := compact_range Φisom.continuous,
id                                  
typ                                 
401        have hΨ : compact (range Ψ) := compact_range Ψisom.continuous,
id                                  
typ                                 
402        apply (Hausdorff_dist_zero_iff_eq_of_closed _ _ _).1 (DΦΨ.symm),
403        { exact closed_of_compact (range Φ) hΦ },
id                                          
typ                                         
st                                                └┘
404        { exact closed_of_compact (range Ψ) hΨ },
id                                          
typ                                         
st                                                └┘
405        { exact Hausdorff_edist_ne_top_of_nonempty_of_bounded (range_nonempty _)
406            (range_nonempty _) hΦ.bounded hΨ.bounded } },
st                                                      └──┘
407      have T : ((range Ψ) ≃ᵢ y.rep) = ((range Φ) ≃ᵢ y.rep), by rw this,
id                                                   └───┘
src                                                    └───┘
typ                                                  └───┘
doc                                                    └───┘
408      have eΨ := cast T Ψisom.isometric_on_range.symm,
409      have e := Φisom.isometric_on_range.trans eΨ,
410      rw [← x.to_GH_space_rep, ← y.to_GH_space_rep, to_GH_space_eq_to_GH_space_iff_isometric],
411      exact ⟨e⟩
412    end,
st     └─┘
413    dist_triangle := λx y z, begin
id                         
typ                        
414      /- To show the triangular inequality between `X`, `Y` and `Z`, realize an optimal coupling
415      between `X` and `Y` in a space `γ1`, and an optimal coupling between `Y`and `Z` in a space `γ2`.
416      Then, glue these metric spaces along `Y`. We get a new space `γ` in which `X` and `Y` are
417      optimally coupled, as well as `Y` and `Z`. Apply the triangle inequality for the Hausdorff
418      distance in `γ` to conclude. -/
419      let X := x.rep,
id                └───┘
src               └───┘
typ               └───┘
doc               └───┘
420      let Y := y.rep,
id                └───┘
src               └───┘
typ               └───┘
doc               └───┘
421      let Z := z.rep,
id                └───┘
src               └───┘
typ               └───┘
doc               └───┘
422      let γ1 := optimal_GH_coupling X Y,
id                                       
typ                                      
423      let γ2 := optimal_GH_coupling Y Z,
id                                      
typ                                     
424      let Φ : Y → γ1 := optimal_GH_injr X Y,
id                  └┘                     
typ                 └┘                     
425      have hΦ : isometry Φ := isometry_optimal_GH_injr X Y,
id                                                        
typ                                                       
426      let Ψ : Y → γ2 := optimal_GH_injl Y Z,
id                  └┘                     
typ                 └┘                     
427      have hΨ : isometry Ψ := isometry_optimal_GH_injl Y Z,
id                                                        
typ                                                       
428      let γ := glue_space hΦ hΨ,
429      letI : metric_space γ := metric.metric_space_glue_space hΦ hΨ,
id              └──────────┘ 
src             └──────────┘
typ             └──────────┘ 
doc             └──────────┘
430      have Comm : (to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y) = (to_glue_r hΦ hΨ) ∘ (optimal_GH_injl Y Z) :=
id                                                                                                    
typ                                                                                                   
431        to_glue_commute hΦ hΨ,
432      calc dist x z = dist (to_GH_space X) (to_GH_space Z) :
433          by rw [x.to_GH_space_rep, z.to_GH_space_rep]
st                                                      
434        ... ≤ Hausdorff_dist (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injl X Y)))
435                         (range ((to_glue_r hΦ hΨ) ∘ (optimal_GH_injr Y Z))) :
436          GH_dist_le_Hausdorff_dist
437            ((to_glue_l_isometry hΦ hΨ).comp (isometry_optimal_GH_injl X Y))
id                                                                        
typ                                                                       
438            ((to_glue_r_isometry hΦ hΨ).comp (isometry_optimal_GH_injr Y Z))
id                                                                         
typ                                                                        
439        ... ≤ Hausdorff_dist (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injl X Y)))
440                             (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y)))
441            + Hausdorff_dist (range ((to_glue_l hΦ hΨ) ∘ (optimal_GH_injr X Y)))
442                             (range ((to_glue_r hΦ hΨ) ∘ (optimal_GH_injr Y Z))) :
443          begin
444            refine Hausdorff_dist_triangle (Hausdorff_edist_ne_top_of_nonempty_of_bounded
445              (range_nonempty _) (range_nonempty _) _ _),
446            { exact (compact_range (isometry.continuous ((to_glue_l_isometry hΦ hΨ).comp
447                (isometry_optimal_GH_injl X Y)))).bounded },
id                                            
typ                                           
st                                                           └┘
448            { exact (compact_range (isometry.continuous ((to_glue_l_isometry hΦ hΨ).comp
449                (isometry_optimal_GH_injr X Y)))).bounded }
id                                            
typ                                           
st                                                           └┘
450          end
st           └─┘
451        ... = Hausdorff_dist ((to_glue_l hΦ hΨ) '' (range (optimal_GH_injl X Y)))
452                             ((to_glue_l hΦ hΨ) '' (range (optimal_GH_injr X Y)))
453            + Hausdorff_dist ((to_glue_r hΦ hΨ) '' (range (optimal_GH_injl Y Z)))
454                             ((to_glue_r hΦ hΨ) '' (range (optimal_GH_injr Y Z))) :
455          by simp only [eq.symm range_comp, Comm, eq_self_iff_true, add_right_inj]
456        ... = Hausdorff_dist (range (optimal_GH_injl X Y))
457                             (range (optimal_GH_injr X Y))
458            + Hausdorff_dist (range (optimal_GH_injl Y Z))
459                             (range (optimal_GH_injr Y Z)) :
460          by rw [Hausdorff_dist_image (to_glue_l_isometry hΦ hΨ),
461                 Hausdorff_dist_image (to_glue_r_isometry hΦ hΨ)]
st                                                                 
462        ... = dist (to_GH_space X) (to_GH_space Y) + dist (to_GH_space Y) (to_GH_space Z) :
463          by rw [Hausdorff_dist_optimal, Hausdorff_dist_optimal, GH_dist, GH_dist]
st                                                                                  
464        ... = dist x y + dist y z:
id                               
typ                              
465          by rw [x.to_GH_space_rep, y.to_GH_space_rep, z.to_GH_space_rep]
st                                                                         
466    end }
st     └─┘
467  
468  end GH_space --section
469  end Gromov_Hausdorff
470  
471  /-- In particular, nonempty compacts of a metric space map to `GH_space`. We register this
472  in the topological_space namespace to take advantage of the notation `p.to_GH_space`. -/
473  definition topological_space.nonempty_compacts.to_GH_space {α : Type u} [metric_space α]
id                                                                              └──┘  └──┘ 
src                                                                             └──┘  └──┘
typ                                                                             └──┘  └──┘ 
doc                                                                             └──┘  └──┘
474    (p : nonempty_compacts α) : Gromov_Hausdorff.GH_space := Gromov_Hausdorff.to_GH_space p.val
id                                └───────────────────────┘
src                                └───────────────────────┘
typ                               └───────────────────────┘
doc                                └───────────────────────┘
475  
476  open topological_space
477  
478  namespace Gromov_Hausdorff
479  
480  section nonempty_compacts
481  variables {α : Type u} [metric_space α]
id                            └─────────┘
src                           └─────────┘
typ                           └─────────┘
doc                           └─────────┘
482  
483  theorem GH_dist_le_nonempty_compacts_dist (p q : nonempty_compacts α) :
id                                                    └───────────────┘ 
src                                                   └───────────────┘
typ                                                   └───────────────┘ 
doc                                                   └───────────────┘
484    dist p.to_GH_space q.to_GH_space ≤ dist p q :=
id     └──┘ └──────────┘ └──────────┘  └──┘  
src    └──┘  └──────────┘  └──────────┘  └──┘
typ    └──┘ └──────────┘ └──────────┘  └──┘  
doc          └──────────┘  └──────────┘
485  begin
st   └─────
486    have ha : isometry (subtype.val : p.val → α) := isometry_subtype_val,
id               └──────┘  └─────────┘   └───┘        └──────────────────┘
src             └──────┘  └─────────┘   └───┘         └──────────────────┘
typ             └──────┘  └─────────┘   └───┘        └──────────────────┘
doc             └──────┘                              └──────────────────┘
txt    
par    
pid    
st   ──┘         └──────┘ └──────────┘   └───┘       └──────────────────┘└─
487    have hb : isometry (subtype.val : q.val → α) := isometry_subtype_val,
id               └──────┘  └─────────┘   └───┘        └──────────────────┘
src              └──────┘  └─────────┘   └───┘         └──────────────────┘
typ              └──────┘  └─────────┘   └───┘        └──────────────────┘
doc              └──────┘                              └──────────────────┘
st   ─┘          └──────┘ └──────────┘   └───┘       └──────────────────┘
488    have A : dist p q = Hausdorff_dist p.val q.val := rfl,
489    have I : p.val = range (subtype.val : p.val → α), by simp,
490    have J : q.val = range (subtype.val : q.val → α), by simp,
491    rw [I, J] at A,
492    rw A,
493    exact GH_dist_le_Hausdorff_dist ha hb
494  end
st   └─┘
495  
496  lemma to_GH_space_lipschitz :
497    lipschitz_with 1 (nonempty_compacts.to_GH_space : nonempty_compacts α → GH_space) :=
id     └────────────┘    └───────────────────────────┘   └───────────────┘    └──────┘
src    └────────────┘    └───────────────────────────┘   └───────────────┘     └──────┘
typ    └────────────┘    └───────────────────────────┘   └───────────────┘    └──────┘
doc    └────────────┘    └───────────────────────────┘   └───────────────┘     └──────┘
498  lipschitz_with.one_mk GH_dist_le_nonempty_compacts_dist
id   └───────────────────┘ └───────────────────────────────┘
src  └───────────────────┘ └───────────────────────────────┘
typ  └───────────────────┘ └───────────────────────────────┘
499  
500  lemma to_GH_space_continuous :
501    continuous (nonempty_compacts.to_GH_space : nonempty_compacts α → GH_space) :=
id     └────────┘  └───────────────────────────┘   └───────────────┘    └──────┘
src    └────────┘  └───────────────────────────┘   └───────────────┘     └──────┘
typ    └────────┘  └───────────────────────────┘   └───────────────┘    └──────┘
doc    └────────┘  └───────────────────────────┘   └───────────────┘     └──────┘
502  to_GH_space_lipschitz.to_continuous
id   └───────────────────┘└────────────┘
src  └───────────────────┘└────────────┘
typ  └───────────────────┘└────────────┘
doc                       └────────────┘
503  
504  end nonempty_compacts
505  
506  section
507  /- In this section, we show that if two metric spaces are isometric up to `ε₂`, then their
508  Gromov-Hausdorff distance is bounded by `ε₂ / 2`. More generally, if there are subsets which are
509  `ε₁`-dense and `ε₃`-dense in two spaces, and isometric up to `ε₂`, then the Gromov-Hausdorff distance
510  between the spaces is bounded by `ε₁ + ε₂/2 + ε₃`. For this, we construct a suitable coupling between
511  the two spaces, by gluing them (approximately) along the two matching subsets. -/
512  
513  variables {α : Type u} [metric_space α] [compact_space α] [nonempty α]
id                          └──────────┘     └───────────┘     └──────┘
src                          └──────────┘     └───────────┘     └──────┘
typ                         └──────────┘     └───────────┘     └──────┘
doc                          └──────────┘     └───────────┘
514            {β : Type v} [metric_space β] [compact_space β] [nonempty β]
id                           └──────────┘     └───────────┘     └──────┘
src                          └──────────┘     └───────────┘     └──────┘
typ                          └──────────┘     └───────────┘     └──────┘
doc                          └──────────┘     └───────────┘
515  
516  -- we want to ignore these instances in the following theorem
517  local attribute [instance, priority 10] sum.topological_space sum.uniform_space
id                                           └───────────────────┘ └───────────────┘
src                                          └───────────────────┘ └───────────────┘
typ                                          └───────────────────┘ └───────────────┘
518  /-- If there are subsets which are `ε₁`-dense and `ε₃`-dense in two spaces, and
519  isometric up to `ε₂`, then the Gromov-Hausdorff distance between the spaces is bounded by
520  `ε₁ + ε₂/2 + ε₃`. -/
521  theorem GH_dist_le_of_approx_subsets {s : set α} (Φ : s → β) {ε₁ ε₂ ε₃ : ℝ}
id                                             └─┘                         
src                                            └─┘                            
typ                                            └─┘                         
522    (hs : ∀x : α, ∃y ∈ s, dist x y ≤ ε₁) (hs' : ∀x : β, ∃y : s, dist x (Φ y) ≤ ε₃)
id                      └──┘    └┘                     └──┘       └┘
src                        └──┘                               └──┘         
typ                     └──┘    └┘                     └──┘       └┘
523    (H : ∀x y : s, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε₂) :
id                   └─┘  └──┘    └──┘           └┘
src                   └─┘  └──┘      └──┘              
typ                  └─┘  └──┘    └──┘           └┘
524    GH_dist α β ≤ ε₁ + ε₂ / 2 + ε₃ :=
id     └─────┘    └┘  └┘     └┘
src    └─────┘                
typ    └─────┘    └┘  └┘     └┘
doc    └─────┘
525  begin
st   └───┘
526    refine real.le_of_forall_epsilon_le (λδ δ0, _),
id                                           
typ                                          
527    rcases exists_mem_of_nonempty α with ⟨xα, _⟩,
id                                   
typ                                  
528    rcases hs xα with ⟨xs, hxs, Dxs⟩,
id               └┘
typ              └┘
529    have sne : s.nonempty := ⟨xs, hxs⟩,
id                               └┘
typ                              └┘
530    letI : nonempty s := sne.to_subtype,
id            └──────┘ 
src           └──────┘
typ           └──────┘ 
531    have : 0 ≤ ε₂ := le_trans (abs_nonneg _) (H ⟨xs, hxs⟩ ⟨xs, hxs⟩),
id                └┘                                          └┘
typ               └┘                                          └┘
532    have : ∀ p q : s, abs (dist p q - dist (Φ p) (Φ q)) ≤ 2 * (ε₂/2 + δ) := λp q, calc
id                                                                └┘     
typ                                                               └┘     
533      abs (dist p q - dist (Φ p) (Φ q)) ≤ ε₂ : H p q
534      ... ≤ 2 * (ε₂/2 + δ) : by linarith,
id                  └┘     
typ                 └┘     
535    -- glue `α` and `β` along the almost matching subsets
536    letI : metric_space (α ⊕ β) := glue_metric_approx (λ x:s, (x:α)) (λx, Φ x) (ε₂/2 + δ) (by linarith) this,
id                                                                              └┘     
typ                                                                             └┘     
537    let Fl := @sum.inl α β,
id                         
typ                        
538    let Fr := @sum.inr α β,
id                         
typ                        
539    have Il : isometry Fl := isometry_emetric_iff_metric.2 (λx y, rfl),
id                        └┘                                     
typ                       └┘                                     
540    have Ir : isometry Fr := isometry_emetric_iff_metric.2 (λx y, rfl),
id                        └┘                                     
typ                       └┘                                     
541    /- The proof goes as follows : the `GH_dist` is bounded by the Hausdorff distance of the images in the
542    coupling, which is bounded (using the triangular inequality) by the sum of the Hausdorff distances
543    of `α` and `s` (in the coupling or, equivalently in the original space), of `s` and `Φ s`, and of
544    `Φ s` and `β` (in the coupling or, equivalently, in the original space). The first term is bounded
545    by `ε₁`, by `ε₁`-density. The third one is bounded by `ε₃`. And the middle one is bounded by `ε₂/2`
546    as in the coupling the points `x` and `Φ x` are at distance `ε₂/2` by construction of the coupling
547    (in fact `ε₂/2 + δ` where `δ` is an arbitrarily small positive constant where positivity is used
548    to ensure that the coupling is really a metric space and not a premetric space on `α ⊕ β`). -/
549    have : GH_dist α β ≤ Hausdorff_dist (range Fl) (range Fr) :=
id                                              └┘         └┘
typ                                             └┘         └┘
550      GH_dist_le_Hausdorff_dist Il Ir,
551    have : Hausdorff_dist (range Fl) (range Fr) ≤ Hausdorff_dist (range Fl) (Fl '' s)
552                                                + Hausdorff_dist (Fl '' s) (range Fr),
id                                                                         
typ                                                                        
553    { have B : bounded (range Fl) := (compact_range Il.continuous).bounded,
id                               └┘
typ                              └┘
554      exact Hausdorff_dist_triangle (Hausdorff_edist_ne_top_of_nonempty_of_bounded
555        (range_nonempty _) (sne.image _) B (B.subset (image_subset_range _ _))) },
st                                                                                 └┘
556    have : Hausdorff_dist (Fl '' s) (range Fr) ≤ Hausdorff_dist (Fl '' s) (Fr '' (range Φ))
id                                                                        
typ                                                                       
557                                               + Hausdorff_dist (Fr '' (range Φ)) (range Fr),
558    { have B : bounded (range Fr) := (compact_range Ir.continuous).bounded,
id                               └┘
typ                              └┘
559      exact Hausdorff_dist_triangle' (Hausdorff_edist_ne_top_of_nonempty_of_bounded
560        ((range_nonempty _).image _) (range_nonempty _)
561        (bounded.subset (image_subset_range _ _) B) B) },
st                                                        └┘
562    have : Hausdorff_dist (range Fl) (Fl '' s) ≤ ε₁,
id                                                 └┘
typ                                                └┘
563    { rw [← image_univ, Hausdorff_dist_image Il],
564      have : 0 ≤ ε₁ := le_trans dist_nonneg Dxs,
id                  └┘                           
typ                 └┘                           
565      refine Hausdorff_dist_le_of_mem_dist this (λx hx, hs x)
id                                            └──┘    └┘  └┘
typ                                           └──┘    └┘  └┘
566        (λx hx, ⟨x, mem_univ _, by simpa⟩) },
id            └┘      └──────┘
src                    └──────┘
typ           └┘      └──────┘
st                                            └┘
567    have : Hausdorff_dist (Fl '' s) (Fr '' (range Φ)) ≤ ε₂/2 + δ,
id            └────────────┘  └┘       └┘     └───┘      └┘     
src           └────────────┘                   └───┘
typ           └────────────┘  └┘       └┘     └───┘      └┘     
doc           └────────────┘                   └───┘
568    { refine Hausdorff_dist_le_of_mem_dist (by linarith) _ _,
569      { assume x' hx',
570        rcases (set.mem_image _ _ _).1 hx' with ⟨x, ⟨x_in_s, xx'⟩⟩,
571        rw ← xx',
572        use [Fr (Φ ⟨x, x_in_s⟩), mem_image_of_mem Fr (mem_range_self _)],
id                     
typ                    
573        exact le_of_eq (glue_dist_glued_points (λ x:s, (x:α)) Φ (ε₂/2 + δ) ⟨x, x_in_s⟩) },
id                                                                 └┘        
typ                                                                └┘        
st                                                                                         └┘
574      { assume x' hx',
575        rcases (set.mem_image _ _ _).1 hx' with ⟨y, ⟨y_in_s', yx'⟩⟩,
576        rcases mem_range.1 y_in_s' with ⟨x, xy⟩,
577        use [Fl x, mem_image_of_mem _ x.2],
578        rw [← yx', ← xy, dist_comm],
id                      └┘
typ                     └┘
579        exact le_of_eq (glue_dist_glued_points (@subtype.val α s) Φ (ε₂/2 + δ) x) } },
id                                                                    └┘     
typ                                                                   └┘     
st                                                                                   └──┘
580    have : Hausdorff_dist (Fr '' (range Φ)) (range Fr) ≤ ε₃,
id                                                          └┘
typ                                                         └┘
581    { rw [← @image_univ _ _ Fr, Hausdorff_dist_image Ir],
id                             └┘
typ                            └┘
582      rcases exists_mem_of_nonempty β with ⟨xβ, _⟩,
id                                     
typ                                    
583      rcases hs' xβ with ⟨xs', Dxs'⟩,
id                  └┘
typ                 └┘
584      have : 0 ≤ ε₃ := le_trans dist_nonneg Dxs',
id                  └┘
typ                 └┘
585      refine Hausdorff_dist_le_of_mem_dist this (λx hx, ⟨x, mem_univ _, by simpa⟩) (λx _, _),
id                                                                                     
typ                                                                                    
586      rcases hs' x with ⟨y, Dy⟩,
id                  
typ                 
587      exact ⟨Φ y, mem_range_self _, Dy⟩ },
st                                         └┘
588    linarith
589  end
st   └─┘
590  end --section
591  
592  /-- The Gromov-Hausdorff space is second countable. -/
593  instance second_countable : second_countable_topology GH_space :=
id                                                         └──────┘
src                                                        └──────┘
typ                                                        └──────┘
doc                                                        └──────┘
594  begin
595    refine second_countable_of_countable_discretization (λδ δpos, _),
596    let ε := (2/5) * δ,
id                      
typ                     
597    have εpos : 0 < ε := mul_pos (by norm_num) δpos,
id                     
typ                    
598    have : ∀p:GH_space, ∃s : set (p.rep), finite s ∧ (univ ⊆ (⋃x∈s, ball x ε)) :=
id               └──────┘             └──┘               └──┘                
src              └──────┘             └──┘               └──┘
typ              └──────┘             └──┘               └──┘                
doc              └──────┘             └──┘
599      λp, by simpa using finite_cover_balls_of_compact (@compact_univ p.rep _ _) εpos,
id                                                                      └───┘
src                                                                      └───┘
typ                                                                     └───┘
doc                                                                      └───┘
600    -- for each `p`, `s p` is a finite `ε`-dense subset of `p` (or rather the metric space
601    -- `p.rep` representing `p`)
602    choose s hs using this,
603    have : ∀p:GH_space, ∀t:set (p.rep), finite t → ∃n:ℕ, ∃e:equiv t (fin n), true,
id               └──────┘     └─┘                                       └─┘     └──┘
src              └──────┘     └─┘                                       └─┘     └──┘
typ              └──────┘     └─┘                                       └─┘     └──┘
doc              └──────┘
604    { assume p t ht,
605      letI : fintype t := finite.fintype ht,
id              └─────┘                    └┘
src             └─────┘
typ             └─────┘                    └┘
doc             └─────┘
606      rcases fintype.exists_equiv_fin t with ⟨n, hn⟩,
id                                       
typ                                      
607      rcases hn with e,
608      exact ⟨n, e, trivial⟩ },
id                   └─────┘
src                   └─────┘
typ                  └─────┘
st                             └┘
609    choose N e hne using this,
610    -- cardinality of the nice finite subset `s p` of `p.rep`, called `N p`
611    let N := λp:GH_space, N p (s p) (hs p).1,
id                 └──────┘
src                └──────┘
typ                └──────┘
doc                └──────┘
612    -- equiv from `s p`, a nice finite subset of `p.rep`, to `fin (N p)`, called `E p`
613    let E := λp:GH_space, e p (s p) (hs p).1,
id                 └──────┘
src                └──────┘
typ                └──────┘
doc                └──────┘
614    -- A function `F` associating to `p : GH_space` the data of all distances between points
615    -- in the `ε`-dense set `s p`.
616    let F : GH_space → Σn:ℕ, (fin n → fin n → ℤ) :=
id             └──────┘                  └─┘
src            └──────┘                  └─┘
typ            └──────┘                  └─┘
doc            └──────┘
617      λp, ⟨N p, λa b, floor (ε⁻¹ * dist ((E p).inv_fun a) ((E p).inv_fun b))⟩,
id                          
typ                         
618    refine ⟨_, by apply_instance, F, λp q hpq, _⟩,
id                                        
typ                                       
619    /- As the target space of F is countable, it suffices to show that two points
620    `p` and `q` with `F p = F q` are at distance `≤ δ`.
621    For this, we construct a map `Φ` from `s p ⊆ p.rep` (representing `p`)
622    to `q.rep` (representing `q`) which is almost an isometry on `s p`, and
623    with image `s q`. For this, we compose the identification of `s p` with `fin (N p)`
624    and the inverse of the identification of `s q` with `fin (N q)`. Together with
625    the fact that `N p = N q`, this constructs `Ψ` between `s p` and `s q`, and then
626    composing with the canonical inclusion we get `Φ`. -/
627    have Npq : N p = N q := (sigma.mk.inj_iff.1 hpq).1,
id                      
typ                     
628    let Ψ : s p → s q := λx, (E q).inv_fun (fin.cast Npq ((E p).to_fun x)),
id                                                           
typ                                                          
629    let Φ : s p → q.rep := λx, Ψ x,
id                  └───┘
src                  └───┘
typ                 └───┘
doc                  └───┘
630    -- Use the almost isometry `Φ` to show that `p.rep` and `q.rep`
631    -- are within controlled Gromov-Hausdorff distance.
632    have main : GH_dist p.rep q.rep ≤ ε + ε/2 + ε,
id                         └───┘ └───┘             
src                        └───┘ └───┘
typ                        └───┘ └───┘             
doc                        └───┘ └───┘
633    { refine GH_dist_le_of_approx_subsets Φ  _ _ _,
634      show ∀x : p.rep, ∃ (y : p.rep) (H : y ∈ s p), dist x y ≤ ε,
id                               └───┘                           
src                              └───┘
typ                              └───┘                           
doc                              └───┘
635      { -- by construction, `s p` is `ε`-dense
636        assume x,
637        have : x ∈ ⋃y∈(s p), ball y ε := (hs p).2 (mem_univ _),
id                                          
typ                                         
638        rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
639        exact ⟨y, ys, le_of_lt hy⟩ },
id                
typ               
st                                    └┘
640      show ∀x : q.rep, ∃ (z : s p), dist x (Φ z) ≤ ε,
id                 └───┘                             
src                └───┘
typ                └───┘                             
doc                └───┘
641      { -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
642        assume x,
643        have : x ∈ ⋃y∈(s q), ball y ε := (hs q).2 (mem_univ _),
id                                          
typ                                         
644        rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
645        let i := ((E q).to_fun ⟨y, ys⟩).1,
id                                
typ                               
646        let hi := ((E q).to_fun ⟨y, ys⟩).2,
id                                 
typ                                
647        have ihi_eq : (⟨i, hi⟩ : fin (N q)) = (E q).to_fun ⟨y, ys⟩, by rw fin.ext_iff,
id                                 └─┘                      
src                                 └─┘
typ                                └─┘                      
648        have hiq : i < N q := hi,
id                        
typ                       
649        have hip : i < N p, { rwa Npq.symm at hiq },
id                        
typ                       
st                                                   └┘
650        let z := (E p).inv_fun ⟨i, hip⟩,
id                                  └─┘
typ                                 └─┘
651        use z,
652        have C1 : (E p).to_fun z = ⟨i, hip⟩ := (E p).right_inv ⟨i, hip⟩,
id                                      └─┘                       └─┘
typ                                     └─┘                       └─┘
653        have C2 : fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl,
id                                    └─┘     
typ                                   └─┘     
654        have C3 : (E q).inv_fun ⟨i, hi⟩ = ⟨y, ys⟩, by { rw ihi_eq, exact (E q).left_inv ⟨y, ys⟩ },
id                                                                                      
typ                                                                                     
st                                                                                                 └┘
655        have : Φ z = y :=
id                      
typ                     
656          by { simp only [Φ, Ψ], rw [C1, C2, C3], refl },
st                                                        └┘
657        rw this,
658        exact le_of_lt hy },
st                           └┘
659      show ∀x y : s p, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε,
id                                                           
typ                                                          
660      { /- the distance between `x` and `y` is encoded in `F p`, and the distance between
661        `Φ x` and `Φ y` (two points of `s q`) is encoded in `F q`, all this up to `ε`.
662        As `F p = F q`, the distances are almost equal. -/
663        assume x y,
664        have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl,
665        rw this,
666        -- introduce `i`, that codes both `x` and `Φ x` in `fin (N p) = fin (N q)`
667        let i := ((E p).to_fun x).1,
id                      
typ                     
668        have hip : i < N p := ((E p).to_fun x).2,
id                                
typ                               
669        have hiq : i < N q, by rwa Npq at hip,
id                        
typ                       
670        have i' : i = ((E q).to_fun (Ψ x)).1, by { simp [Ψ, (E q).right_inv _] },
id                                                              
typ                                                             
st                                                                                └┘
671        -- introduce `j`, that codes both `y` and `Φ y` in `fin (N p) = fin (N q)`
672        let j := ((E p).to_fun y).1,
id                      
typ                     
673        have hjp : j < N p := ((E p).to_fun y).2,
id                                
typ                               
674        have hjq : j < N q, by rwa Npq at hjp,
id                        
typ                       
675        have j' : j = ((E q).to_fun (Ψ y)).1, by { simp [Ψ, (E q).right_inv _] },
id                                                              
typ                                                             
st                                                                                └┘
676        -- Express `dist x y` in terms of `F p`
677        have : (F p).2 ((E p).to_fun x) ((E p).to_fun y) = floor (ε⁻¹ * dist x y),
id                                                                  
typ                                                                 
678          by simp only [F, (E p).left_inv _],
id                               
typ                              
679        have Ap : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = floor (ε⁻¹ * dist x y),
id                             └─┘     └─┘           
typ                            └─┘     └─┘           
680          by { rw ← this, congr; apply (fin.ext_iff _ _).2; refl },
id                                                             └──┘
src                                                            └──┘
typ                                                            └──┘
doc                                                            └──┘
st                                                                  └┘
681        -- Express `dist (Φ x) (Φ y)` in terms of `F q`
682        have : (F q).2 ((E q).to_fun (Ψ x)) ((E q).to_fun (Ψ y)) = floor (ε⁻¹ * dist (Ψ x) (Ψ y)),
id                                                                          
typ                                                                         
683          by simp only [F, (E q).left_inv _],
id                               
typ                              
684        have Aq : (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩ = floor (ε⁻¹ * dist (Ψ x) (Ψ y)),
id                             └─┘     └─┘           
typ                            └─┘     └─┘           
685          by { rw ← this, congr; apply (fin.ext_iff _ _).2; [exact i', exact j'] },
st                                                                                  └┘
686        -- use the equality between `F p` and `F q` to deduce that the distances have equal
687        -- integer parts
688        have : (F p).2 ⟨i, hip⟩ ⟨j, hjp⟩ = (F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩,
id                           └─┘      └─┘              └─┘     └─┘
typ                          └─┘      └─┘              └─┘     └─┘
689        { -- we want to `subst hpq` where `hpq : F p = F q`, except that `subst` only works
690          -- with a constant, so replace `F q` (and everything that depends on it) by a constant `f`
691          -- then `subst`
692          revert hiq hjq,
693          change N q with (F q).1,
id                            
typ                           
694          generalize_hyp : F q = f at hpq ⊢,
id                              
typ                             
695          subst hpq,
696          intros,
697          refl },
st                └┘
698        rw [Ap, Aq] at this,
699        -- deduce that the distances coincide up to `ε`, by a straightforward computation
700        -- that should be automated
701        have I := calc
702          abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) =
703            abs (ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))) : (abs_mul _ _).symm
id                  
typ                 
704          ... = abs ((ε⁻¹ * dist x y) - (ε⁻¹ * dist (Ψ x) (Ψ y))) : by { congr, ring }
st                                                                                      └┘
705          ... ≤ 1 : le_of_lt (abs_sub_lt_one_of_floor_eq_floor this),
706        calc
707          abs (dist x y - dist (Ψ x) (Ψ y)) = (ε * ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) :
id                                                    
typ                                                   
708            by rw [mul_inv_cancel (ne_of_gt εpos), one_mul]
st                                                           
709          ... = ε * (abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y))) :
710            by rw [abs_of_nonneg (le_of_lt (inv_pos εpos)), mul_assoc]
st                                                                      
711          ... ≤ ε * 1 : mul_le_mul_of_nonneg_left I (le_of_lt εpos)
712          ... = ε : mul_one _ } },
st                               └──┘
713    calc dist p q = GH_dist (p.rep) (q.rep) : dist_GH_dist p q
id                              └───┘   └───┘                  
src                             └───┘   └───┘
typ                             └───┘   └───┘                  
doc                             └───┘   └───┘
714      ... ≤ ε + ε/2 + ε : main
id                       
typ                      
715      ... = δ : by { simp [ε], ring }
id                           
typ                          
st                                     └─
716  end
st   ──┘
717  
718  /-- Compactness criterion: a closed set of compact metric spaces is compact if the spaces have
719  a uniformly bounded diameter, and for all `ε` the number of balls of radius `ε` required
720  to cover the spaces is uniformly bounded. This is an equivalence, but we only prove the
721  interesting direction that these conditions imply compactness. -/
722  lemma totally_bounded {t : set GH_space} {C : ℝ} {u : ℕ → ℝ} {K : ℕ → ℕ}
id                                 └──────┘                           
src                                └──────┘                           
typ                                └──────┘                           
doc                                 └──────┘
723    (ulim : tendsto u at_top (𝓝 0))
724    (hdiam : ∀p ∈ t, diam (univ : set (GH_space.rep p)) ≤ C)
id                                  └┘   └┘  └┘  └┘        
src                                  └┘   └┘  └┘  └┘
typ                                 └┘   └┘  └┘  └┘        
doc                                       └┘  └┘  └┘
725    (hcov : ∀p ∈ t, ∀n:ℕ, ∃s : set (GH_space.rep p), cardinal.mk s ≤ K n ∧ univ ⊆ ⋃x∈s, ball x (u n)) :
id                                     └──┘  └──┘                                            
src                                     └──┘  └──┘                         
typ                                    └──┘  └──┘                                            
doc                                      └──┘  └──┘
726    totally_bounded t :=
id                     
typ                    
727  begin
728    /- Let `δ>0`, and `ε = δ/5`. For each `p`, we construct a finite subset `s p` of `p`, which
729    is `ε`-dense and has cardinality at most `K n`. Encoding the mutual distances of points in `s p`,
730    up to `ε`, we will get a map `F` associating to `p` finitely many data, and making it possible to
731    reconstruct `p` up to `ε`. This is enough to prove total boundedness. -/
732    refine metric.totally_bounded_of_finite_discretization (λδ δpos, _),
id                                                              
typ                                                             
733    let ε := (1/5) * δ,
id                      
typ                     
734    have εpos : 0 < ε := mul_pos (by norm_num) δpos,
id                     
typ                    
735    -- choose `n` for which `u n < ε`
736    rcases metric.tendsto_at_top.1 ulim ε εpos with ⟨n, hn⟩,
id                                         
typ                                        
737    have u_le_ε : u n ≤ ε,
id                       
typ                      
738    { have := hn n (le_refl _),
id                  
typ                 
739      simp only [real.dist_eq, add_zero, sub_eq_add_neg, neg_zero] at this,
740      exact le_of_lt (lt_of_le_of_lt (le_abs_self _) this) },
st                                                            └┘
741    -- construct a finite subset `s p` of `p` which is `ε`-dense and has cardinal `≤ K n`
742    have : ∀p:GH_space, ∃s : set (p.rep), ∃N ≤ K n, ∃E : equiv s (fin N),
id               └──────┘       └─┘   └──┘       
src              └──────┘       └─┘   └──┘
typ              └──────┘       └─┘   └──┘       
doc              └──────┘             └──┘
743      p ∈ t → univ ⊆ ⋃x∈s, ball x (u n),
id              └──┘                 
src              └──┘
typ             └──┘                 
744    { assume p,
745      by_cases hp : p ∉ t,
id                       
src                      
typ                      
746      { have : nonempty (equiv (∅ : set (p.rep)) (fin 0)),
id                └──────┘  └───┘      └─┘  └───┘    └─┘
src               └──────┘  └───┘      └─┘  └───┘    └─┘
typ               └──────┘  └───┘      └─┘  └───┘    └─┘
doc                         └───┘           └───┘
747        { rw ← fintype.card_eq, simp },
st                                      └┘
748        use [∅, 0, bot_le, choice (this)] },
st                                           └┘
749      { rcases hcov _ (set.not_not_mem.1 hp) n with ⟨s, ⟨scard, scover⟩⟩,
id                                              
typ                                             
750        rcases cardinal.lt_omega.1 (lt_of_le_of_lt scard (cardinal.nat_lt_omega _)) with ⟨N, hN⟩,
751        rw [hN, cardinal.nat_cast_le] at scard,
752        have : cardinal.mk s = cardinal.mk (fin N), by rw [hN, cardinal.mk_fin],
id                               └─────────┘  └─┘ 
src                               └─────────┘  └─┘
typ                              └─────────┘  └─┘ 
doc                               └─────────┘
st                                                                               
753        cases quotient.exact this with E,
754        use [s, N, scard, E],
id                 
typ                
755        simp [hp, scover] } },
st                           └──┘
756    choose s N hN E hs using this,
757    -- Define a function `F` taking values in a finite type and associating to `p` enough data
758    -- to reconstruct it up to `ε`, namely the (discretized) distances between elements of `s p`.
759    let M := (floor (ε⁻¹ * max C 0)).to_nat,
id                                   └────┘
src                                    └────┘
typ                                  └────┘
760    let F : GH_space → (Σk:fin ((K n).succ), (fin k → fin k → fin (M.succ))) :=
id             └──────┘       └─┘     └──┘                          └────┘
src            └──────┘                 └──┘                          └────┘
typ            └──────┘       └─┘     └──┘                          └────┘
doc            └──────┘
761      λp, ⟨⟨N p, lt_of_le_of_lt (hN p) (nat.lt_succ_self _)⟩,
id            
typ           
762           λa b, ⟨min M (floor (ε⁻¹ * dist ((E p).inv_fun a) ((E p).inv_fun b))).to_nat,
id                                                                               └────┘
src                                                                                └────┘
typ                                                                              └────┘
763                  lt_of_le_of_lt ( min_le_left _ _) (nat.lt_succ_self _) ⟩ ⟩,
764    refine ⟨_, by apply_instance, (λp, F p), _⟩,
765    -- It remains to show that if `F p = F q`, then `p` and `q` are `ε`-close
766    rintros ⟨p, pt⟩ ⟨q, qt⟩ hpq,
767    have Npq : N p = N q := (fin.ext_iff _ _).1 (sigma.mk.inj_iff.1 hpq).1,
id                      
typ                     
768    let Ψ : s p → s q := λx, (E q).inv_fun (fin.cast Npq ((E p).to_fun x)),
id                                                           
typ                                                          
769    let Φ : s p → q.rep := λx, Ψ x,
id                  └───┘
src                  └───┘
typ                 └───┘
doc                  └───┘
770    have main : GH_dist (p.rep) (q.rep) ≤ ε + ε/2 + ε,
id                          └───┘   └───┘              
src                         └───┘   └───┘
typ                         └───┘   └───┘              
doc                         └───┘   └───┘
771    { -- to prove the main inequality, argue that `s p` is `ε`-dense in `p`, and `s q` is `ε`-dense
772      -- in `q`, and `s p` and `s q` are almost isometric. Then closeness follows
773      -- from `GH_dist_le_of_approx_subsets`
774      refine GH_dist_le_of_approx_subsets Φ  _ _ _,
775      show ∀x : p.rep, ∃ (y : p.rep) (H : y ∈ s p), dist x y ≤ ε,
id                               └───┘                           
src                              └───┘
typ                              └───┘                           
doc                              └───┘
776      { -- by construction, `s p` is `ε`-dense
777        assume x,
778        have : x ∈ ⋃y∈(s p), ball y (u n) := (hs p pt) (mem_univ _),
id                                             
typ                                            
779        rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
780        exact ⟨y, ys, le_trans (le_of_lt hy) u_le_ε⟩ },
id                                             └────┘
typ                                            └────┘
st                                                      └┘
781      show ∀x : q.rep, ∃ (z : s p), dist x (Φ z) ≤ ε,
id                 └───┘                             
src                └───┘
typ                └───┘                             
doc                └───┘
782      { -- by construction, `s q` is `ε`-dense, and it is the range of `Φ`
783        assume x,
784        have : x ∈ ⋃y∈(s q), ball y (u n) := (hs q qt) (mem_univ _),
id                                             
typ                                            
785        rcases mem_bUnion_iff.1 this with ⟨y, ys, hy⟩,
786        let i := ((E q).to_fun ⟨y, ys⟩).1,
id                                
typ                               
787        let hi := ((E q).to_fun ⟨y, ys⟩).2,
id                                 
typ                                
788        have ihi_eq : (⟨i, hi⟩ : fin (N q)) = (E q).to_fun ⟨y, ys⟩, by rw fin.ext_iff,
id                                 └─┘                      
src                                 └─┘
typ                                └─┘                      
789        have hiq : i < N q := hi,
id                        
typ                       
790        have hip : i < N p, { rwa Npq.symm at hiq },
id                        
typ                       
st                                                   └┘
791        let z := (E p).inv_fun ⟨i, hip⟩,
id                                  └─┘
typ                                 └─┘
792        use z,
793        have C1 : (E p).to_fun z = ⟨i, hip⟩ := (E p).right_inv ⟨i, hip⟩,
id                                      └─┘                       └─┘
typ                                     └─┘                       └─┘
794        have C2 : fin.cast Npq ⟨i, hip⟩ = ⟨i, hi⟩ := rfl,
id                                    └─┘     
typ                                   └─┘     
795        have C3 : (E q).inv_fun ⟨i, hi⟩ = ⟨y, ys⟩, by { rw ihi_eq, exact (E q).left_inv ⟨y, ys⟩ },
id                                                                                      
typ                                                                                     
st                                                                                                 └┘
796        have : Φ z = y :=
id                      
typ                     
797          by { simp only [Φ, Ψ], rw [C1, C2, C3], refl },
st                                                        └┘
798        rw this,
799        exact le_trans (le_of_lt hy) u_le_ε },
id                                      └────┘
typ                                     └────┘
st                                             └┘
800      show ∀x y : s p, abs (dist x y - dist (Φ x) (Φ y)) ≤ ε,
id                                                           
typ                                                          
801      { /- the distance between `x` and `y` is encoded in `F p`, and the distance between
802        `Φ x` and `Φ y` (two points of `s q`) is encoded in `F q`, all this up to `ε`.
803        As `F p = F q`, the distances are almost equal. -/
804        assume x y,
805        have : dist (Φ x) (Φ y) = dist (Ψ x) (Ψ y) := rfl,
806        rw this,
807        -- introduce `i`, that codes both `x` and `Φ x` in `fin (N p) = fin (N q)`
808        let i := ((E p).to_fun x).1,
id                      
typ                     
809        have hip : i < N p := ((E p).to_fun x).2,
id                                
typ                               
810        have hiq : i < N q, by rwa Npq at hip,
id                        
typ                       
811        have i' : i = ((E q).to_fun (Ψ x)).1, by { simp [Ψ, (E q).right_inv _] },
id                                                              
typ                                                             
st                                                                                └┘
812        -- introduce `j`, that codes both `y` and `Φ y` in `fin (N p) = fin (N q)`
813        let j := ((E p).to_fun y).1,
id                      
typ                     
814        have hjp : j < N p := ((E p).to_fun y).2,
id                                
typ                               
815        have hjq : j < N q, by rwa Npq at hjp,
id                        
typ                       
816        have j' : j = ((E q).to_fun (Ψ y)).1, by { simp [Ψ, (E q).right_inv _] },
id                                                              
typ                                                             
st                                                                                └┘
817        -- Express `dist x y` in terms of `F p`
818        have Ap : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = (floor (ε⁻¹ * dist x y)).to_nat := calc
id                              └─┘     └─┘               
typ                             └─┘     └─┘               
819          ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F p).2 ((E p).to_fun x) ((E p).to_fun y)).1 :
id                                                                       
typ                                                                      
820            by { congr; apply (fin.ext_iff _ _).2; refl }
st                                                         └┘
821          ... = min M (floor (ε⁻¹ * dist x y)).to_nat :
id                     
typ                    
822            by simp only [F, (E p).left_inv _]
id                                 
typ                                
823          ... = (floor (ε⁻¹ * dist x y)).to_nat :
id                         
typ                        
824          begin
825            refine min_eq_right (int.to_nat_le_to_nat (floor_mono _)),
826            refine mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) (le_of_lt (inv_pos εpos)),
827            change dist (x : p.rep) y ≤ C,
id                              └───┘      
src                             └───┘
typ                             └───┘      
doc                             └───┘
828            refine le_trans (dist_le_diam_of_mem compact_univ.bounded (mem_univ _) (mem_univ _)) _,
829            exact hdiam p pt
id                         
typ                        
830          end,
st           └─┘
831        -- Express `dist (Φ x) (Φ y)` in terms of `F q`
832        have Aq : ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = (floor (ε⁻¹ * dist (Ψ x) (Ψ y))).to_nat := calc
id                              └─┘     └─┘               
typ                             └─┘     └─┘               
833          ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1 = ((F q).2 ((E q).to_fun (Ψ x)) ((E q).to_fun (Ψ y))).1 :
id                                                                           
typ                                                                          
834            by { congr; apply (fin.ext_iff _ _).2; [exact i', exact j'] }
st                                                                         └┘
835          ... = min M (floor (ε⁻¹ * dist (Ψ x) (Ψ y))).to_nat :
id                     
typ                    
836            by simp only [F, (E q).left_inv _]
id                                 
typ                                
837          ... = (floor (ε⁻¹ * dist (Ψ x) (Ψ y))).to_nat :
id                         
typ                        
838          begin
839            refine min_eq_right (int.to_nat_le_to_nat (floor_mono _)),
840            refine mul_le_mul_of_nonneg_left (le_trans _ (le_max_left _ _)) (le_of_lt (inv_pos εpos)),
841            change dist (Ψ x : q.rep) (Ψ y) ≤ C,
id                                └───┘          
src                               └───┘
typ                               └───┘          
doc                               └───┘
842            refine le_trans (dist_le_diam_of_mem compact_univ.bounded (mem_univ _) (mem_univ _)) _,
843            exact hdiam q qt
id                         
typ                        
844          end,
st           └─┘
845        -- use the equality between `F p` and `F q` to deduce that the distances have equal
846        -- integer parts
847        have : ((F p).2 ⟨i, hip⟩ ⟨j, hjp⟩).1 = ((F q).2 ⟨i, hiq⟩ ⟨j, hjq⟩).1,
id                            └┘       └┘                   └┘      └┘
typ                           └┘       └┘                   └┘      └┘
848        { -- we want to `subst hpq` where `hpq : F p = F q`, except that `subst` only works
849          -- with a constant, so replace `F q` (and everything that depends on it) by a constant `f`
850          -- then `subst`
851          revert hiq hjq,
852          change N q with (F q).1,
id                            
typ                           
853          generalize_hyp : F q = f at hpq ⊢,
id                              
typ                             
854          subst hpq,
855          intros,
856          refl },
st                └┘
857        have : floor (ε⁻¹ * dist x y) = floor (ε⁻¹ * dist (Ψ x) (Ψ y)),
id                                                
typ                                               
858        { rw [Ap, Aq] at this,
859          have D : 0 ≤ floor (ε⁻¹ * dist x y) :=
id                               
typ                              
860            floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos εpos)) dist_nonneg),
861          have D' : floor (ε⁻¹ * dist (Ψ x) (Ψ y)) ≥ 0 :=
id                            
typ                           
862            floor_nonneg.2 (mul_nonneg (le_of_lt (inv_pos εpos)) dist_nonneg),
863          rw [← int.to_nat_of_nonneg D, ← int.to_nat_of_nonneg D', this] },
st                                                                         └┘
864        -- deduce that the distances coincide up to `ε`, by a straightforward computation
865        -- that should be automated
866        have I := calc
867          abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) =
868            abs (ε⁻¹ * (dist x y - dist (Ψ x) (Ψ y))) : (abs_mul _ _).symm
id                  
typ                 
869          ... = abs ((ε⁻¹ * dist x y) - (ε⁻¹ * dist (Ψ x) (Ψ y))) : by { congr, ring }
st                                                                                      └┘
870          ... ≤ 1 : le_of_lt (abs_sub_lt_one_of_floor_eq_floor this),
871        calc
872          abs (dist x y - dist (Ψ x) (Ψ y)) = (ε * ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y)) :
id                                                    
typ                                                   
873            by rw [mul_inv_cancel (ne_of_gt εpos), one_mul]
st                                                           
874          ... = ε * (abs (ε⁻¹) * abs (dist x y - dist (Ψ x) (Ψ y))) :
875            by rw [abs_of_nonneg (le_of_lt (inv_pos εpos)), mul_assoc]
st                                                                      
876          ... ≤ ε * 1 : mul_le_mul_of_nonneg_left I (le_of_lt εpos)
877          ... = ε : mul_one _ } },
st                               └──┘
878    calc dist p q = GH_dist (p.rep) (q.rep) : dist_GH_dist p q
id                              └───┘   └───┘                  
src                             └───┘   └───┘
typ                             └───┘   └───┘                  
doc                             └───┘   └───┘
879      ... ≤ ε + ε/2 + ε : main
id                       
typ                      
880      ... = δ/2 : by { simp [ε], ring }
id                              
typ                             
st                                       └┘
881      ... < δ : half_lt_self δpos
id             
typ            
882  end
st   └─┘
883  
884  section complete
885  
886  /- We will show that a sequence `u n` of compact metric spaces satisfying
887  `dist (u n) (u (n+1)) < 1/2^n` converges, which implies completeness of the Gromov-Hausdorff space.
888  We need to exhibit the limiting compact metric space. For this, start from
889  a sequence `X n` of representatives of `u n`, and glue in an optimal way `X n` to `X (n+1)`
890  for all `n`, in a common metric space. Formally, this is done as follows.
891  Start from `Y 0 = X 0`. Then, glue `X 0` to `X 1` in an optimal way, yielding a space
892  `Y 1` (with an embedding of `X 1`). Then, consider an optimal gluing of `X 1` and `X 2`, and
893  glue it to `Y 1` along their common subspace `X 1`. This gives a new space `Y 2`, with an
894  embedding of `X 2`. Go on, to obtain a sequence of spaces `Y n`. Let `Z0` be the inductive
895  limit of the `Y n`, and finally let `Z` be the completion of `Z0`.
896  The images `X2 n` of `X n` in `Z` are at Hausdorff distance `< 1/2^n` by construction, hence they
897  form a Cauchy sequence for the Hausdorff distance. By completeness (of `Z`, and therefore of its
898  set of nonempty compact subsets), they converge to a limit `L`. This is the nonempty
899  compact metric space we are looking for.  -/
900  
901  variables (X : ℕ → Type) [∀n, metric_space (X n)] [∀n, compact_space (X n)] [∀n, nonempty (X n)]
id                               └──────────┘           └───────────┘           └──────┘    
src                                └──────────┘             └───────────┘             └──────┘
typ                              └──────────┘           └───────────┘           └──────┘    
doc                                └──────────┘             └───────────┘
902  
903  /-- Auxiliary structure used to glue metric spaces below, recording an isometric embedding
904  of a type `A` in another metric space. -/
905  structure aux_gluing_struct (A : Type) [metric_space A] : Type 1 :=
id                                    └──┘   └──────────┘ 
src                                          └──────────┘
typ                                   └──┘   └──────────┘ 
doc                                          └──────────┘
906  (space  : Type)
id             └──┘
typ            └──┘
907  (metric : metric_space space)
id             └──────────┘ └───┘
src            └──────────┘
typ            └──────────┘ └───┘
doc            └──────────┘
908  (embed  : A → space)
id               └───┘
typ              └───┘
909  (isom   : isometry embed)
id             └──────┘ └───┘
src            └──────┘
typ            └──────┘ └───┘
doc            └──────┘
910  
911  /-- Auxiliary sequence of metric spaces, containing copies of `X 0`, ..., `X n`, where each
912  `X i` is glued to `X (i+1)` in an optimal way. The space at step `n+1` is obtained from the space
913  at step `n` by adding `X (n+1)`, glued in an optimal way to the `X n` already sitting there. -/
914  def aux_gluing (n : ℕ) : aux_gluing_struct (X n) := nat.rec_on n
id                           └───────────────┘        └────────┘ 
src                          └───────────────┘          └────────┘
typ                          └───────────────┘        └────────┘ 
doc                           └───────────────┘
915    { space  := X 0,
id                 
typ                
916      metric := by apply_instance,
917      embed  := id,
id                 └┘
src                └┘
typ                └┘
918      isom   := λx y, rfl }
id                     └─┘
src                      └─┘
typ                    └─┘
919  (λn a, by letI : metric_space a.space := a.metric; exact
id                  └┘  └┘  └┘   └┘  └┘     └──┘  └┘  └┘  
src                   └┘  └┘  └┘   └┘  └┘     └──┘  └┘  └┘  
typ                 └┘  └┘  └┘   └┘  └┘     └──┘  └┘  └┘  
doc                   └┘  └┘  └┘                        └┘  
920    { space  := glue_space a.isom (isometry_optimal_GH_injl (X n) (X n.succ)),
id                 └─┘ └┘  └┘
src                └─┘ └┘  └┘
typ                └─┘ └┘  └┘
921      metric := metric.metric_space_glue_space a.isom (isometry_optimal_GH_injl (X n) (X n.succ)),
id                 └┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
src                └┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
typ                └┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘ └─┘
922      embed  := (to_glue_r a.isom (isometry_optimal_GH_injl (X n) (X n.succ)))
id                  └──┘ └─┘  └┘ └┘
src                 └──┘ └─┘  └┘ └┘
typ                 └──┘ └─┘  └┘ └┘
923                ∘ (optimal_GH_injr (X n) (X n.succ)),
id                   └┘  └┘  └┘  └┘
src                  └┘  └┘  └┘  └┘
typ                  └┘  └┘  └┘  └┘
doc                   └┘  └┘  └┘  └┘
924      isom   := (to_glue_r_isometry _ _).comp (isometry_optimal_GH_injr (X n) (X n.succ)) })
id                                         └┘                                     └────┘
src                                        └┘                                      └────┘
typ                                        └┘                                     └────┘
doc                                        └┘ 
925  
926  /-- The Gromov-Hausdorff space is complete. -/
927  instance : complete_space (GH_space) :=
id              └────────────┘  └──────┘
src             └────────────┘  └──────┘
typ             └────────────┘  └──────┘
doc             └────────────┘  └──────┘
928  begin
st   └─────
929    have : ∀ (n : ℕ), 0 < ((1:ℝ) / 2) ^ n, by { apply _root_.pow_pos, norm_num },
id                                    
src                                   
typ                                   
st   ─┘                                                                           └┘
930    -- start from a sequence of nonempty compact metric spaces within distance `1/2^n` of each other
931    refine metric.complete_of_convergent_controlled_sequences (λn, (1/2)^n) this (λu hu, _),
id                                                                            └──┘   
typ                                                                           └──┘   
932    -- `X n` is a representative of `u n`
933    let X := λn, (u n).rep,
id                     └─┘
src                      └─┘
typ                    └─┘
doc                      └─┘
934    -- glue them together successively in an optimal way, getting a sequence of metric spaces `Y n`
935    let Y := aux_gluing X,
id              └────────┘ 
src             └────────┘
typ             └────────┘ 
doc             └────────┘
936    letI : ∀n, metric_space (Y n).space := λn, (Y n).metric,
id               └──────────┘     └───┘            └────┘
src               └──────────┘      └───┘              └────┘
typ              └──────────┘     └───┘            └────┘
doc               └──────────┘
937    have E : ∀n:ℕ, glue_space (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)) = (Y n.succ).space :=
id                    └────────┘      └──┘                                     └───┘             └───┘
src                   └────────┘      └──┘                                      └───┘              └───┘
typ                   └────────┘      └──┘                                     └───┘             └───┘
938      λn, by { simp [Y, aux_gluing], refl },
id                       └────────┘
src                        └────────┘
typ                      └────────┘
doc                        └────────┘
st                                           └┘
939    let c := λn, cast (E n),
id                 └──┘
src                 └──┘
typ                └──┘
940    have ic : ∀n, isometry (c n) := λn x y, rfl,
id                                     
typ                                    
941    -- there is a canonical embedding of `Y n` in `Y (n+1)`, by construction
942    let f : Πn, (Y n).space → (Y n.succ).space :=
id                                  └───┘
src                                  └───┘
typ                                 └───┘
943      λn, (c n) ∘ (to_glue_l (aux_gluing X n).isom (isometry_optimal_GH_injl (X n) (X n.succ))),
id                                                                                    
typ                                                                                   
944    have I : ∀n, isometry (f n),
id               
typ              
945    { assume n,
946      apply isometry.comp,
947      { assume x y, refl },
st                          └┘
948      { apply to_glue_l_isometry } },
st                                  └──┘
949    -- consider the inductive limit `Z0` of the `Y n`, and then its completion `Z`
950    let Z0 := metric.inductive_limit I,
951    let Z := uniform_space.completion Z0,
id                                       └┘
typ                                      └┘
952    let Φ := to_inductive_limit I,
953    let coeZ := (coe : Z0 → Z),
id                        └┘   
typ                       └┘   
954    -- let `X2 n` be the image of `X n` in the space `Z`
955    let X2 := λn, range (coeZ ∘ (Φ n) ∘ (Y n).embed),
id                         └──┘
typ                        └──┘
956    have isom : ∀n, isometry (coeZ ∘ (Φ n) ∘ (Y n).embed),
id                              └──┘
typ                             └──┘
957    { assume n,
958      apply isometry.comp completion.coe_isometry _,
959      apply isometry.comp _ (Y n).isom,
id                                
typ                               
960      apply to_inductive_limit_isometry },
st                                         └┘
961    -- The Hausdorff distance of `X2 n` and `X2 (n+1)` is by construction the distance between
962    -- `u n` and `u (n+1)`, therefore bounded by `1/2^n`
963    have D2 : ∀n, Hausdorff_dist (X2 n) (X2 n.succ) < (1/2)^n,
id                
typ               
964    { assume n,
965      have X2n : X2 n = range ((coeZ ∘ (Φ n.succ) ∘ (c n)
id                  └┘             └──┘
typ                 └┘             └──┘
966        ∘ (to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))))
967        ∘ (optimal_GH_injl (X n) (X n.succ))),
id                                     └────┘
src                                    └────┘
typ                                    └────┘
968      { change X2 n = range (coeZ ∘ (Φ n.succ) ∘ (c n)
id                              └──┘
typ                             └──┘
969          ∘ (to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ)))
970          ∘ (optimal_GH_injl (X n) (X n.succ))),
id                                       └────┘
src                                      └────┘
typ                                      └────┘
971        simp only [X2, Φ],
id                    └┘
typ                   └┘
972        rw [← to_inductive_limit_commute I],
973        simp only [f],
974        rw ← to_glue_commute },
st                              └┘
975      rw range_comp at X2n,
976      have X2nsucc : X2 n.succ = range ((coeZ ∘ (Φ n.succ) ∘ (c n)
id                      └┘                  └──┘
typ                     └┘                  └──┘
977        ∘ (to_glue_r (Y n).isom (isometry_optimal_GH_injl (X n) (X n.succ))))
978        ∘ (optimal_GH_injr (X n) (X n.succ))), by refl,
979      rw range_comp at X2nsucc,
980      rw [X2n, X2nsucc, Hausdorff_dist_image, Hausdorff_dist_optimal, ← dist_GH_dist],
981      { exact hu n n n.succ (le_refl n) (le_succ n) },
id                      └────┘                      
src                     └────┘
typ                     └────┘                      
st                                                     └┘
982      { apply isometry.comp completion.coe_isometry _,
983        apply isometry.comp _ ((ic n).comp (to_glue_r_isometry _ _)),
id                                    
typ                                   
984        apply to_inductive_limit_isometry } },
st                                           └──┘
985    -- consider `X2 n` as a member `X3 n` of the type of nonempty compact subsets of `Z`, which
986    -- is a metric space
987    let X3 : ℕ → nonempty_compacts Z := λn, ⟨X2 n,
id                                            └┘
typ                                           └┘
988      ⟨range_nonempty _, compact_range (isom n).continuous ⟩⟩,
989    -- `X3 n` is a Cauchy sequence by construction, as the successive distances are
990    -- bounded by `(1/2)^n`
991    have : cauchy_seq X3,
992    { refine cauchy_seq_of_le_geometric (1/2) 1 (by norm_num) (λn, _),
id                                                                 
typ                                                                
993      rw one_mul,
994      exact le_of_lt (D2 n) },
id                          
typ                         
st                             └┘
995    -- therefore, it converges to a limit `L`
996    rcases cauchy_seq_tendsto_of_complete this with ⟨L, hL⟩,
997    -- the images of `X3 n` in the Gromov-Hausdorff space converge to the image of `L`
998    have M : tendsto (λn, (X3 n).to_GH_space) at_top (𝓝 L.to_GH_space) :=
id                        
typ                       
999      tendsto.comp (to_GH_space_continuous.tendsto _) hL,
1000    -- By construction, the image of `X3 n` in the Gromov-Hausdorff space is `u n`.
1001    have : ∀n, (X3 n).to_GH_space = u n,
id                                    
typ                                   
1002    { assume n,
1003      rw [nonempty_compacts.to_GH_space, ← (u n).to_GH_space_rep,
id                                              
typ                                             
1004          to_GH_space_eq_to_GH_space_iff_isometric],
1005      constructor,
1006      convert (isom n).isometric_on_range.symm,
id                     
typ                    
1007    },
st     └┘
1008    -- Finally, we have proved the convergence of `u n`
1009    exact ⟨L.to_GH_space, by simpa [this] using M⟩
1010  end
st   └─┘
1011  
1012  end complete--section
1013  
1014  end Gromov_Hausdorff --namespace